Finding counterexamples to ∀∃ hyperproperties
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.
Tue 16 JanDisplayed time zone: London change
14:00 - 15:30 | Concurrency, Security, & Hyper-propertiesIncorrectness at Mountbatten Exhibition Chair(s): Azalea Raad Imperial College London | ||
14:00 22mTalk | Quantitative Weakest Hyper Pre Incorrectness Linpeng Zhang University College London, Benjamin Lucien Kaminski Saarland University; University College London File Attached | ||
14:22 23mTalk | A Reachability Logic for a Weak Memory Model with Promises Incorrectness Lara Bargmann University of Oldenburg, Brijesh Dongol University of Surrey, Heike Wehrheim University of Oldenburg File Attached | ||
14:45 22mTalk | Towards Temporal Adversarial Logic Incorrectness Julien Vanegue Bloomberg, USA | ||
15:07 22mTalk | Finding counterexamples to ∀∃ hyperproperties Incorrectness DOI Pre-print |