RHLE: Modular Deductive Verification of Relational ∀∃ Properties
summary
RHLE defines a deductive logic and verifier for relational ∀∃ properties by turning implementation nondeterminism into choice variables in function specifications (ghost-like specs) and using a weakest-precondition semantics to generate SMT queries. The Haskell tool uses Z3 and checks a suite of benchmarks from the literature; all but one refinement case verify (one returns unknown due to undecidable quantifiers). The logic is sound, supports modular specs, and the implementation is on GitHub.
AI-written summary · about
chapters (12)
- 0:00Start
- 5:37Universal Hoare Logic
- 8:24Choice variable instantiation corresponds to execution path
- 9:08Existential Hoare Logic
- 9:54Relational Properties
- 10:55k-Safety Properties
- 12:11RHLE: Relational Hoare Logic with Existentials
- 13:09Example 3 Properties
- 15:01Loop Synchronization
- 15:31Key Theorems
- 16:08Automated Verification
- 18:29Summary
related talks
13mEncode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
40mRelational Reasoning in Object-based Programs
15mModular Verification of Op-Based CRDTs in Separation Logic
28mReasoning about Distributed Reconfigurable Systems
17mModular Verification of Safe Memory Reclamation in Concurrent Separation Logic
01h 05mVerifying Infinitely Many Programs at Once
15mData-Driven Abductive Inference of Library Specifications
14mSynthesizing Implication Lemmas for Interactive Theorem Proving