Hypra: A Deductive Program Verifier for Hyper Hoare Logic
summary
Claims the first automated deductive technique for arbitrary hyperproperties by encoding sets of program states explicitly into an intermediate language and discharging verification with an SMT-backed Viper toolchain. Hypra generates Viper encodings that track S and S' and splits S' into S'_exists and S'_forall to avoid SMT matching loops. Implements loop rules and error reasoning, verifies and disproves properties, and scales: 84 benchmark programs, 93% finish within 5 seconds. Encodes both universal and existential quantifier alternations in hyper assertions.
AI-written summary · about
chapters (8)
- 0:00Introduction to Hypra
- 2:27Automating Hyper Hoare Logic
- 4:59Designing Hypra verifier
- 8:36Encoding commands in Viper
- 10:22Matching loops in SMT
- 13:38Solving loops with bounds
- 15:01Evaluation results
- 16:49Q&A
related talks
42mQuantum program analysis: Verification and Testing
17mA HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite(…)
15mGradual Verification of Recursive Heap Data Structures
46mIntroduction to Formal Verification with Symbiotic EDA Open Source Tools
43mHydra's Heads – Dmitriy Ivanov
31mA Comparison of Program Logics for (In)Correctness
18mPreview: Verification (Correctness)
21mTesting APIs the Hypermedia way