On Symmetry and Quantification: A New Approach to Verify Distributed Protocols
Talkat 50 Years of Satisfiability: The Centrality of SAT in the Theory of Computing · 2021-02-11..05-13
summary
Claims that symmetry→quantification yields compact, automatically derived inductive invariants for unbounded parameterized protocols, implemented as an IC3 extension called IC3PO that reads IV/Ivy/TLA+ models and uses AVR for finite-instance checking. On 29 benchmark protocols I4 only proves 13 automatically, while IC3PO derives quantified invariants (e.g. from 3-3-3 instances) that generalize; IC3PO proves all 11 alternation-requiring cases where FOLIC3 proves nine and produces much smaller invariants.
AI-written summary · about
chapters (21)
- 0:00Introduction
- 7:40Infinite State Protocols
- 11:16I4 Protocol Verification
- 14:02I3PO
- 14:26Example
- 16:42Notation
- 18:15quorums
- 19:23full symmetry
- 20:13circuit diagrams
- 23:18equations
- 25:59Incremental induction
- 28:54Boosting Learning
- 29:33Quantification
- 31:57Permuting
- 33:19Question
- 38:24Results
- 41:16Cardano Protocol
- 44:56Questions
- 45:48Undesirability
- 46:49Other Protocols
- 48:00Discussion