Automating Relational Verification of Infinite-State Programs
summary
Two automated approaches appear: a constraint-based pipeline that encodes simultaneous synthesis of a semantic scheduler and relational invariant into an extended CHC class (PFW-style constraints) with fairness and well‑foundedness encodings, and an inductive proof search over a first‑order fixpoint logic modulo theories that unfolds definitions and applies induction lemmas. The implementation (PCAT / muSIC family) solves 15 of 20 benchmark problems fully automatically, uses SMT and CHC backends, and synthesizes Skolem strategies and ranking functions for GNI and co‑termination.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:05What is relational verification
- 6:35Program equivalence and refinement
- 13:10Goals and scope
- 13:53Challenges in relational verification
- 26:10Automating relational verification
- 39:10Limitations and future directions
- 40:14Entertainment checking in fix-point logic
- 49:39Experiments and limitations
- 51:54Conclusion
- 52:57Q&A
related talks
45mAutomated Verification meets Differential Privacy
17mA Deductive System for Contract Satisfaction Proofs
26mVerification of Programs with Concealed Components
12mAutomated Synthesis of Verified Firewalls
19mMechanized Logical Relations for Termination-Insensitive Noninterference
28mProving Memory Access Violations in Isabelle/HOL
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
06mFormal Verification with the Certora Prover