Hyper Separation Logic
summary
Introduces a logic that supports hyperproperties with arbitrary quantifier alternation over heap programs, proves soundness in Isabelle/HOL, and ships reusable artifacts. Key technical steps are a novel hyper separating conjunction and a generalized frame rule that composes universal and existential quantifiers to express GNI and other ∃∀ patterns; handles allocation and non-local errors via “unknown states” and adds scaffold variables for a practical assertion syntax.
AI-written summary · about
chapters (8)
- 0:00Hyper Separation Logic intro
- 1:53Separation Logic vs hyperproperties
- 3:36State set reasoning power
- 7:12Generalized frame rule
- 10:24Hyper separating conjunction
- 16:10Non-locality solutions
- 17:15Summary and future work
- 17:36Q&A
related talks
20mHyper Hoare Logic: (Dis-)Proving Program Hyperproperties
20mAsynchronous Probabilistic Couplings in Higher-Order Separation Logic
57mSequential Information Flow
26mNon-Interference Preserving and Optimising Compilation with Hyperproperty Simulations
21mDecision and Complexity of Dolev-Yao Hyperproperties
19mA quantitative probabilistic relational Hoare logic
34mSymbolic Abstract Heaps for Polymorphic Information-flow Guard Inference
58mAutomating Relational Verification of Infinite-State Programs