POPL 2024 (series) / Incorrectness 2024 (series) / Formal Methods for Incorrectness 2024 /
Quantitative Weakest Hyper Pre
Tue 16 Jan 2024 14:00 - 14:22 at Mountbatten Exhibition - Concurrency, Security, & Hyper-properties Chair(s): Azalea Raad
We present a novel \emph{weakest pre calculus} for \emph{reasoning about quantitative hyperproperties} over \emph{non-deterministic programs}. Whereas existing quantitative weakest pre allows reasoning about the expected or anticipated values that a quantity assumes after program termination from a \emph{single initial state}, we do so for \emph{initial sets of states} or \emph{initial probability distributions}. We thus (i) obtain a weakest pre calculus for hyper Hoare logic and (ii) enable reasoning about so-called \emph{hyperquantities} such as expected values and variances.
slides (sample.pdf) | 306KiB |
Tue 16 JanDisplayed time zone: London change
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 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 |