POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom

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 Jan

Displayed time zone: London change

14:00 - 15:30
Concurrency, Security, & Hyper-propertiesIncorrectness at Mountbatten Exhibition
Chair(s): Azalea Raad Imperial College London
14:00
22m
Talk
Quantitative Weakest Hyper Pre
Incorrectness
Linpeng Zhang University College London, Benjamin Lucien Kaminski Saarland University; University College London
File Attached
14:22
23m
Talk
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
22m
Talk
Towards Temporal Adversarial Logic
Incorrectness
Julien Vanegue Bloomberg, USA
15:07
22m
Talk
Finding counterexamples to ∀∃ hyperproperties
Incorrectness
DOI Pre-print