A Hoare Logic For Symmetry Properties
summary
Defines a Hoare-style program logic where pre/post assertions are composable group actions (syntax for group operations and entailment), implements a prototype tool SymVerif, and uses it to automatically verify symmetry claims on several handcrafted benchmarks. Main technical claim: symmetry preservation reduces to checking entailment between actions and loop-body rules, weakest-precondition exists sometimes, fails otherwise. Result: tool reproduces examples and uncovers an error in McLachlan and Quispel model, artifacts evaluated and functional.
AI-written summary · about
chapters (9)
- 0:00Symmetry properties introduction
- 1:03Symmetry in voting and CPS
- 2:26Formalizing symmetry with group theory
- 3:31Group actions and state
- 5:36Program logic with group actions
- 6:39Verifying car movement
- 8:04Loop invariants and preservation
- 11:32Conclusion and contributions
- 12:38Q&A
related talks
31mCertified Static and Dynamic Symmetry Breaking
20mOn Extending Incorrectness Logic with Backwards Reasoning
22mExecution Time Program Verification With Tight Bounds
23mSpecifying and Verifying Future Conditions
27mUnrealizability Logic
17mA HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite(…)
01h 05mVerifying Infinitely Many Programs at Once
40mRelational Reasoning in Object-based Programs