Axe 'Em: Eliminating Spurious States with Induction Axioms

on YouTube ↗20m

" summary

First-order abstractions get refined into well-founded or finite-domain semantics by instantiating an induction axiom schema guided by finitely representable symbolic countermodels; the paper proves a sound, complete reduction into the Ordered Self-Cycle (OSC) fragment and shows decidability of these semantics in OSC. A prototype tool constructs symbolic models, extracts axioms, and finishes verification on 15 benchmarks (3 distributed, 6 linked-list, 6 network topologies) in under a minute each, eliminating the spurious infinite models.

AI-written summary · about

" chapters (13)

1. 0:00Eliminating spurious states
2. 0:20Introduction
3. 1:02First-order logic modeling
4. 3:12Refining with induction
5. 3:34Paxos verification example
6. 5:43Infinite counter models
7. 7:10Induction axioms
8. 8:36Automating refinement
9. 11:26Completeness limits
10. 12:09OSC fragment results
11. 15:01Tool evaluation
12. 16:05Conclusion
13. 16:26Q&A