Quantitative Strongest Post
This work addresses program verification challenges for researchers in formal methods and programming languages, though it appears incremental as it builds on existing quantitative weakest preconditions.
The authors developed a quantitative strongest-postcondition calculus for reasoning about non-deterministic programs with loops, enabling analysis of quantitative information flow through programs, and introduced the novel concept of strongest liberal postconditions.
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.