Verifying Dafny Contract Integrity
summary
Tool automatically inserts Dafny-generated assertions (via Dafny rewriters) and asks Boogie/Z3 whether four specific pitfalls occur: contradiction, vacuity, unconstrained outputs, redundancy. It reports failing assertions and points to the affected clause, runs inside a Dafny branch, and finds real issues in several test files (including missing coverage of an output case). It currently fails to handle existential quantification witnesses and treats reports as warnings rather than guaranteed bugs.
AI-written summary · about
chapters (11)
- 0:00Contract integrity verification
- 1:29Daphne 4.4 features
- 2:56Detecting specification contradictions
- 3:39Vacuous contract clauses
- 4:45Unconstrained output pitfalls
- 7:33Redundant contract clauses
- 9:20Daphne backend verification
- 10:25Tool demo: binary search
- 11:31Daphne programs testing
- 13:17Limitations and future work
- 14:40Q&A
related talks
01h 02mLanguage Design meets Verifying Compilers
15mOn the Impact of Formal Verification on Software Development
13mMetamorph: Synthesizing Large Objects from Dafny Specifications
36mStatic Analysis of APL for Tooling and Compliance
15mAutomatic Synthesis of Data-Flow Analyzers
24mProving False in Object Oriented Verification Programs by Exploiting Non-Termination
01h 17mFunction Contracts in Practice using C++
14mScalability and Precision by Combining Expressive Type Systems and Deductive Verification