SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Thu 8 Dec 2022 16:30 - 17:00 at Seminar Room G007 - Verification Chair(s): Dominique Devriese

We present a novel strongest-postcondition-style calculus for quantitative reasoning about non-deterministic programs with loops. Whereas existing quantitative weakest pre allows reasoning about the value of a quantity after a program terminates on a given initial state, quantitative strongest post allows reasoning about the value that a quantity had before the program was executed and reached a given final state. We show how strongest post enables reasoning about the flow of quantitative information through programs. Similarly to weakest liberal preconditions, we also develop a quantitative strongest liberal post. As a byproduct, we obtain the entirely unexplored notion of strongest liberal postconditions and show how these foreshadow a potential new program logic - partial incorrectness logic - which would be a more liberal version of O’Hearn’s recent incorrectness logic.

Thu 8 Dec

Displayed time zone: Auckland, Wellington change

15:30 - 17:00
VerificationOOPSLA at Seminar Room G007
Chair(s): Dominique Devriese KU Leuven
15:30
30m
Talk
Checking Equivalence in a Non-strict Language
OOPSLA
John C. Kolesar Yale University, Ruzica Piskac Yale University, William T. Hallahan Yale University
DOI
16:00
30m
Talk
Necessity Specifications for Robustness
OOPSLA
Julian Mackay Victoria University of Wellington, Susan Eisenbach Imperial College London, James Noble Research & Programming, Sophia Drossopoulou Meta and Imperial College London
DOI
16:30
30m
Research paper
Quantitative strongest post: a calculus for reasoning about the flow of quantitative information
OOPSLA
Linpeng Zhang University College London, Benjamin Lucien Kaminski Saarland University and University College London
DOI