Counterexample Driven Quantifier Instantiations with Applications to Distribute...
summary
Replaces problematic function symbols with a one-to-one relational abstraction inside Ivy and drives refinements by solver counterexamples; SMT solvers that diverge on the original verification condition now either prove goals or produce concrete spurious models. Applied to consensus (including PBFT variants) and exported to C++; most inductive checks verify automatically, only a few manual instantiations are needed, and the method is complete w.r.t. first-order logic (finitely many refinements eliminate spurious countermodels).
AI-written summary · about
chapters (13)
- 0:00Introduction
- 0:22Motivation for distributed protocols
- 1:48Goals and challenges
- 2:53Decidable over undecidable logic
- 4:00Previous approaches limitations
- 4:42Simple consensus example
- 7:17Verification and inductive invariant
- 8:00Relational obstruction abstraction
- 9:30Counterexample-driven instantiation
- 10:40Experimental results applications
- 11:23Key advantages
- 12:24Automation versus expressiveness
- 13:10Q&A on completeness
related talks
26mUnification for Subformula Linking under Quantifiers
14mSynthesizing Implication Lemmas for Interactive Theorem Proving
48mBeyond SAT - Proofs for QBF, and more
15mIncremental Certified Programming
01h 05mVerifying Infinitely Many Programs at Once
23mSeparating the Wheat from the Chaff: Understanding (In-)Completeness of Proof(…)
20mOn Extending Incorrectness Logic with Backwards Reasoning
28mReasoning about Distributed Reconfigurable Systems