Portfolio Solving for Dafny
summary
A cloud-hosted portfolio runs multiple SMT engines (Z3 4.2.1, 4.8.5, newer Z3, CVC5, Vampire) against the same 177k‑LOC Dafny repo with ~14k VCs and returns the first conclusive result or compares all outputs. Using three Z3 versions plus others yields ~25% median speedup and cuts hard VCs significantly; Z3 4.2.1 uniquely solves a handful that newer Z3 times out on; CVC5 wins 5.9% of queries giving a 12.1% time improvement, Vampire wins 0.3% for a 7.2% gain. cloud-hosted solvers compete vs waitall
AI-written summary · about
chapters (9)
- 0:00Portfolio solving for Dafny
- 1:24How Dafny verification works
- 3:09Why proofs fail in Dafny
- 4:54Solving proof brittleness
- 5:38Designing multi-solver portfolios
- 7:43Testing solver performance
- 12:24Adopting alternative SMT solvers
- 14:51Results and conclusion
- 15:37Q&A
related talks
20mRandomised Testing of the Dafny Compiler: Into the CI
10m{ Fast, Cost-effective } – Choose Two
24mSupercharging CI: Test Suite Optimization for Speed, Stability, and Savings
01h 45mRun Frontier AI at Home
37mYou can be a World Champion!
17mCarlos Guestrin, CEO of Dato Inc. @ MLconf SEA
26mEmpirical Complexity of Laplacian Solvers: A Discussion
42mSupercharge Your Performance with the Optimus Cirrus Platform