How To Make Formal Methods A Software Quality Solution That Can Actually Be Used In The Industry
summary
Formal methods are presented as exhaustive for given input ranges via value analysis and abstract interpretation, guaranteeing no false negatives while still producing false positives; formal proofs require contracts (ACSL or C++ contracts) and run much slower (example: value analysis in ~10s vs proof in ~3+ minutes). A concrete industrial benchmark is ~12,000 LOC analyzed in 5–10 minutes on a VM yielding 84 errors found. Practical adoption requires IDE integration, fast iterative analyses, low false‑positive density, and contracts embedded in C++ to avoid extra languages.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 1:08What are formal methods
- 5:26Formal methods approaches
- 9:23Value analysis and abstract interpretation
- 13:22Why formal methods rarely used
- 14:49Challenges in adoption
- 16:59Simplifying accessibility
- 19:49Perception of lengthy analyses
- 21:55Optimizing analysis speed
- 24:45Reducing false positives
- 29:52Requirements for adoption
- 31:18Functional verification
- 33:51Performance trade-offs
- 34:57C++ contracts integration
- 36:00Conclusions and future
- 41:23Q&A
related talks
46mKeynote: Formal Verification? No, Formal Reasoning!
15mOn the Impact of Formal Verification on Software Development
22mFormal Runtime Error Detection During Development in the Automotive Industry
23mSpecifying and Verifying Future Conditions
21mMechanised Hypersafety Proofs about Structured Data
01h 05mVerifying Infinitely Many Programs at Once
03mInterview
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems