Verified VCG and Verified Compiler for Dafny
summary
Builds a functional big‑step semantics for an imperative subset of Dafny and proves a verified VCG and verified compiler that translate Dafny (mutual recursion, while loops, arrays, McCarthy 91) to CakeML, then to machine code, preserving behavior; proofs are fully mechanized in HOL4 and show semantic equivalence between source and compiled code, implementation zero‑initializes locals to avoid undefined references, VCs are generated as weakest preconditions and validated with theorem‑prover tactics.
AI-written summary · about
chapters (8)
- 0:00Verified VCG and compiler intro
- 2:27Motivation behind project
- 4:13Dafny to KKML compiler
- 7:43Semantics for correctness
- 8:47Verified verification condition generator
- 14:03Putting pieces together
- 14:25Future work and conclusion
- 15:33Q&A
related talks
18mBaking for Dafny: A CakeML Backend for Dafny
19mLean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean
01h 05mMuch Still to Do in Compiler Verification (A Perspective from the CakeML Project)
01h 02mLanguage Design meets Verifying Compilers
14mEmbedding Quantum Program Verification into Dafny
19mVelvet: A Multi-Modal Verifier for Effectful Programs
17mPureCake: A Verified Compiler for a Lazy Functional Language
24mCakes That Bake Cakes: Dynamic Computation in CakeML