Model checking algorithms for hyperproperties (invited paper)

DOI10.1007/978-3-030-67067-2_1zbMath1472.68088arXiv2107.11841OpenAlexW3118247109MaRDI QIDQ2234054

Bernd Finkbeiner

Publication date: 18 October 2021

Full work available at URL: https://arxiv.org/abs/2107.11841

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items

Generalized arrays for Stainless frames

Cites Work

• From liveness to promptness
• Algorithms for model checking HyperLTL and HyperCTL\(^*\)
• Realizing \(\omega\)-regular hyperproperties
• Unifying Hyper and Epistemic Temporal Logics
• Secure information flow by self-composition
• The First-Order Logic of Hyperproperties
• Verifying hyperliveness
• Unnamed Item