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…