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

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 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