Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
This conference talk from POPL 2025 presents research on coinductive proof techniques for temporal hyperproperties, specifically focusing on hyperliveness properties. Learn how researchers Arthur Correnson and Bernd Finkbeiner from CISPA Helmholtz Center for Information Security tackle the challenge of verifying hyperproperties with alternating universal and existential quantification over system executions. Discover their novel approach showing that hyperproperties of the form $\forall^\exists^\psi$ (where $\psi$ is a safety relation) can be approximated by coinductive relations, enabling intuitive proofs by coinduction. The presentation introduces HyCo (Hyperproperties, Coinductively), a mechanized framework implemented within the Coq proof assistant for reasoning about temporal hyperproperties. See practical applications of this framework for verifying reactive systems modeled as imperative programs with nondeterminism and I/O. The research includes reusable artifacts available through Zenodo, making it valuable for researchers and practitioners working in formal verification and temporal logic.
