1 citations · 1 across the 4 of their papers we have counts for
4 papers
Verified VCG and Verified Compiler for Dafny
Daniel Nezamabadi, Magnus O. Myreen, Yong Kiam Tan
Dafny is a verification-aware programming language that comes with a compiler and static program verifier. However, neither the compiler nor the verifier is proved correct; in fact…
Faster Certified Symmetry Breaking Using Orders With Auxiliary Variables
Markus Anders, Bart Bogaerts, Benjamin Bogø +8
Symmetry breaking is a crucial technique in modern combinatorial solving, but it is difficult to be sure it is implemented correctly. The most successful approach to deal with bugs…
Baking for Dafny: A CakeML Backend for Dafny
Daniel Nezamabadi, Magnus Myreen
Dafny is a verification-aware programming language that allows developers to formally specify their programs and prove them correct. Currently, a Dafny program is compiled in two s…
Certified MaxSAT Preprocessing
Hannes Ihalainen, Andy Oertel, Yong Kiam Tan +3
Building on the progress in Boolean satisfiability (SAT) solving over the last decades, maximum satisfiability (MaxSAT) has become a viable approach for solving NP-hard optimizatio…