Coinductive Proofs for Temporal Hyperliveness

on YouTube ↗20m

" summary

Framework shows that every forall∃ψ hyperproperty with ψ a safety relation admits a coinductive approximation, enabling incremental witness construction via parameterized coinduction. The authors build HyCo, mechanized in Coq, prove its soundness (proof uses the axiom of choice), and apply it to verify reactive imperative programs with nondeterminism and I/O. Implementation and evaluated artifacts are available (Zenodo); the logic is sound but not complete, and probabilistic or prophecy extensions remain future work.

AI-written summary · about

" chapters (11)

1. 0:00Introduction
2. 0:23Coinductive proofs for hyperproperties
3. 1:05Hyperproperties for reactive systems
4. 3:34Formalizing non-interference
5. 4:37Verifying hyperproperties challenges
6. 7:03HIO proof framework
7. 9:59Proof rules for relational invariance
8. 12:28Local and incremental proofs
9. 13:53Limitations and future work
10. 15:18Resources and conclusion
11. 15:40Q&A