Helping users to reduce Brittleness in their Dafny programs - a success story
summary
Dafny adds three concrete features that cut proof brittleness: assertion isolation (split proofs into assertion batches), hide and reveal (exclude function bodies from SMT unless needed), and opaque blocks (collapse many heap mutations into one layer). Brittleness is measured by SMT resource count and by mutating proofs thousands of times; an example moves verification from 11s to 16s, a brittle proof shows high relative standard deviation (~1.4+) and many timeouts, and AWS code reports large resource reductions in practice.
AI-written summary · about
chapters (15)
- 0:00Reducing brittleness in Dafny
- 0:49Brittleness in Dafny proofs
- 2:36Measuring proof brittleness
- 4:03Resource count and brittleness
- 5:07Assertion isolation in Dafny
- 7:16Advanced assertion isolation
- 8:40Assertion isolation impact
- 9:44Function hiding to reduce complexity
- 11:50Opaque blocks for large methods
- 13:13Opaque blocks simplify verification
- 15:22Performance impact of opaque blocks
- 16:24Features and future work
- 17:32Q&A: Resource count
- 18:57Q&A: Opaque blocks use
- 19:41Q&A: Heap layer in opaque blocks
related talks
01h 02mLanguage Design meets Verifying Compilers
46mRefinement Types from Light to Deep Verification
21mVerified VCG and Verified Compiler for Dafny
19mVelvet: A Multi-Modal Verifier for Effectful Programs
03mAttempts to design hardware using dafny
14mEmbedding Quantum Program Verification into Dafny
17mCode-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…)
19mPanel: Compilation Frameworks