Dafny Test Generation
summary
DTest generates executable unit and system tests by inserting failing assertions, asking the Dafny verifier for counterexamples, and extracting concrete inputs from Z3 models; it scales via selective inlining to produce system-level tests that use a single entry point and cover deep call paths. It finds provably unreachable dead code, produced hundreds of tests for real projects (including AWS ESDK), and achieves high branch coverage while letting users trade off coverage for speed.
AI-written summary · about
chapters (5)
- 0:00Introduction
- 1:04Dafny test toolkit
- 7:24System-level tests challenges
- 10:36User-guided inlining
- 12:24Results and Q&A
related talks
20mRandomised Testing of the Dafny Compiler: Into the CI
18mSMT2Test: From SMT Formulas to Effective Test Cases
42mSimulation Testing
26mDifferential Testing with Foundry
47mTDD & Generative AI: A Perfect Pairing
25mTesting in production: Ideas, experiences, limits, roadblocks
42mEffective Developer Testing: taking it to the next level
01h 31mTest-Driven Data Analysis