Domesticating Automation
summary
Proposes a module-granular view of the quantifier instantiation graph and a crude metric that ranks modules by how many downstream instantiations they enable, then applies it to a 20,000-line VUS key-value store. Identifies a surprising hotspot in a buffer_seek module, makes a problematic predicate opaque definition, and cuts instantiations from about 100,000 → 33,000, yielding roughly a 2x verification speedup while revealing limits of the metric.
AI-written summary · about
chapters (8)
- 0:00Automation at scale intro
- 1:52Quantifier instantiation trade-offs
- 3:59Diagnosing automation issues
- 5:44Module-based automation control
- 8:53Quantifier instantiation case study
- 10:57Refactoring instantiation overhead
- 12:42Limitations and future directions
- 13:23Pushing automation further
related talks
37mModularization - flatten your graph and get the real benefits
30mSolid Modularization - Untangling the dependency graph
50mMajestic Modular Monoliths
41mBreaking the build
01h 04mModular Monoliths and Other Facepalms
25mFrom Continuous Profiling to Continuous Optimization
42mScan, Patch, VEX - Using Open Source Tools to Manage...
01h 02mModern CMake Modules