Hyper Hoare Logic: Proving and Disproving Program Hyperproperties

Explore a groundbreaking 20-minute video presentation from PLDI 2024 that introduces Hyper Hoare Logic, a novel approach to proving and disproving program hyperproperties. Delve into how this generalization of Hoare logic expands the capabilities of formal program verification by allowing assertions over arbitrary sets of states. Learn how this simple yet expressive logic can reason about both the absence and existence of program executions, enabling the verification of properties that were previously beyond the reach of existing Hoare logics. Discover the logic's soundness, completeness, and its ability to capture important proof principles naturally. Gain insights into the potential applications of Hyper Hoare Logic in areas such as functional correctness, determinism, and non-interference. Presented by Thibault Dardinier and Peter Müller from ETH Zurich, this talk offers a comprehensive overview of their research, which has been formally verified in Isabelle/HOL and comes with reusable artifacts for further exploration.

[PLDI24] Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties