An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Dedu...
summary
Proposes a finite, machine-checkable representation of certain infinite first-order models called symbolic structures and encodes model checking into linear integer arithmetic so solvers can validate them. Builds a template-driven symbolic search that compiles into LIA queries and implements it as the Fast tool. Proves a decidable fragment OSC that strictly extends EPR and guarantees a small symbolic model. Evaluated on 21 benchmarks: linked-list examples <1s, distributed-protocols average <1min, worst ≈2min, while Z3/cvc5/Vampire diverge or return unknown.
AI-written summary · about
chapters (12)
- 0:00Infinite counter-models in verification
- 1:30Infinite counter-models in SMT solvers
- 2:33Domains with infinite models
- 3:57Paxos verification example
- 4:59Structure of infinite counter-model
- 6:00Finite symbolic representation
- 8:28Checking formulas against models
- 8:50Searching satisfying models
- 10:18OSC fragment of first-order logic
- 12:07Tool implementation with Fast
- 13:34Conclusion and future work
- 14:39Questions and answers session
related talks
22mOptimizing Optimizations: Case Study on Detecting Specific Types of Mathematical(…)
01h 04mEDSL Infinity Wars: Mainstreaming Symbolic Computation
21mChecking Equivalence in a Non-strict Language
16mCompositional Symbolic Execution for the Next 700 Memory Models
22mCounterexample-Guided Inference of Modular Specifications
13mProgram Analysis via Efficient Symbolic Abstraction
18mLanguages with Decidable Learning: A Meta-theorem
31mLetting users do the undecidable: lessons from program synthesis