Finding counterexamples to ∀∃ hyperproperties
summary
An algorithm searches for counterexamples to ∀∃-safety hyperproperties in infinite-state software by picking symbolic execution paths for the universal quantifiers and checking a fixed-structure bounded model checking query with an SMT solver for the existential replies, iteratively refining path constraints when spurious results arise. It maps asynchronous observations via OHyperLTL-style projection, struggles with divergence (unbounded loops) and undecidable theory fragments, and produces concrete traces but not yet human-friendly existential certificates. Evaluation on Bner 2022 and RHLE benchmarks finds many RHLE counterexamples, with three diverging cases and five cases requiring division.
AI-written summary · about
chapters (15)
- 0:00Counterexample finding for hyperproperties
- 1:04Incorrectness in hyperproperty verification
- 2:28Observational determinism example
- 3:32Challenges in refinement verification
- 4:58Limitations of verification approaches
- 6:22O-hyperLTL for async systems
- 8:09Symbolic execution basics
- 8:50Symbolic execution + BMC approach
- 10:53Finite traces in temporal logics
- 12:58Divergence in bound model checking
- 14:24Meaningful counterexamples for ∃
- 15:51Non-interference with higher quantifiers
- 16:54Benchmark results
- 19:06Q&A: Unrolling depth & path explosion
- 21:14Q&A: Quantifier reordering & symbolic execution