Nießen, T., & Weissenbacher, G. (2024, January 16). Finding counterexamples to ∀∃ hyperproperties [Conference Presentation]. Formal Methods for Incorrectness 2024, London, United Kingdom of Great Britain and Northern Ireland (the). https://doi.org/10.34726/5455
Verification of software systems against hyperproperties that require quantifier alternation among the quantified trace variables is notoriously difficult because it generally cannot be reduced to the verification of single-trace properties. Such hyperproperties include the class of ∀∃-safety hyperproperties, which contains important hyperproperties such as refinement and generalized non-interference. Existing approaches to the verification of these properties are often incomplete or restricted to finite-state systems. When the hyperproperty does not hold, no existing approaches can fully automatically produce counterexamples demonstrating this fact. We present an algorithm that searches for counterexamples to ∀∃-safety hyperproperties in infinite-state software systems and evaluate its effectiveness based on existing examples from related works.
Logics for Computer Science Program at TU Wien: 101034440 (European Commission)