Abstract Interpretation, Software Model Checking, and Beyond - A Celebration of the(…)
summary
A retrospective of SLAM’s engineering and theory: a C-to-Boolean pipeline that under-approximates correlations (SLAM’s actual abstraction is Cartesian abstraction, not the ideal Boolean abstraction), powered deployment of static driver verifier on Windows from 2004 for about 20 years, and seeded tools like Z3 and Coral. Contributions include a practical synthesis of linear ranking functions for termination, a framing of abstraction refinement as oracle-guided widening, and empirical benchmarks that propelled SV-COMP and widespread industrial use.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 1:4825 years of SLAM project
- 3:12Software model checking rise
- 5:40Static Driver Verifier impact
- 8:07Abstract interpretation meets SLAM
- 13:50Cartesian abstraction in SLAM
- 14:52Termination and lattices
- 16:17Abstraction refinement completeness
- 18:23Ranking functions for termination
- 20:48Postlude reflections
- 21:54SLAM legacy and tools
- 24:01Modern model checking benchmarks
- 25:23Teaching drivers with micro:bit
- 26:28Newton algorithm and Craig interpolation
- 28:14Symbolic automata directions
- 29:17Learning specifications from behavior
- 31:06Q&A
related talks
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
52mThink Abstractly, Work Concretely
01h 05mVerifying Infinitely Many Programs at Once
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
34mLogic in Computer Science, Engineering and Industry
58mA New Perspective on Commutativity in Verification
28mBounded Model Checking of PLC ST Programs using Rewriting Modulo SMT
29müberSpark: Enforcing Verifiable Object Abstractions for Automated...