My Journey to the Dark Side: Under-Approximation, Incorrectness, Proof
summary
Talk describes concrete methods and outcomes: an analyzer built with an abstract interpreter and abduction summaries runs in CI, finds 25,000 race bugs in a year, and scales to hundreds of thousands of lines by using compositional summaries and fractional permissions. The design deliberately embraces under-approximation (proofs of bug presence, not absence), trades soundness for usefulness under stated assumptions, and ships an incremental, developer-friendly tool that actually worked in production.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:24From academia to industry
- 5:13Scaling program analysis
- 9:02Concurrency and the RaceD tool
- 13:26Engineering vs theory
- 28:12The logic of incorrectness
- 30:43Abduction and under-approximation
- 48:31Q&A session
related talks
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
18mPreview: Verification (Correctness & Debugging)
57mVariant analysis
43mCracking the Code Review: from Guesswork to Automated Guidance
29mLessons from Zero-Defect Software
18mPreview: Verification (Correctness)
01h 07mSufficiently Advanced Testing
21mAbstract Debuggers: Exploring Program Behaviors Using Static Analysis Results