Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties
summary
Logic lifts pre/postconditions to properties of arbitrary sets of states and claims to capture exactly the class of hyperproperties over terminating executions, enabling both proving and disproving hyperproperties (including non-interference, determinism, K-safety, existential reachability). Core development gives nine core rules plus syntactic rules for loops and composition, the metatheory is sound and complete, and all results are mechanized in Isabelle/HOL with reusable artifacts and examples.
AI-written summary · about
chapters (8)
- 0:00Hyperproperties introduction
- 2:33Hyper Hoare Logic core
- 5:41Hyper triples for properties
- 7:07Logical tags for relations
- 9:54Core rules for triples
- 13:06Syntactic rules for reasoning
- 15:14Summary and future
- 15:35Q&A
related talks
21mHyper Separation Logic
19mHeterogeneous Dynamic Logic: Provability Modulo Program Theories
20mA Taxonomy of Hoare-Like Logics
16mA Hoare-Logic Style Refinement Types Formalisation
19mA quantitative probabilistic relational Hoare logic
26mNon-Interference Preserving and Optimising Compilation with Hyperproperty Simulations
59mTowards static analyses and abstract domains for hyperproperties
21mDecision and Complexity of Dolev-Yao Hyperproperties