Quantitative strongest post: a calculus for reasoning about the flow of quantitative inform
summary
Presents a formal calculus that defines a quantitative strongest post and a strongest liberal post for nondeterministic programs with loops, where predicates become quantities (states → extended reals) and existential/for-all quantifiers become supremum/infimum with min/max and indicator functions mapped to ±∞. Gives syntactic rules for assignment, composition and loops (least/greatest fixed points), proves Galois connections with WP/WLP, and shows an explicit info‑flow example where algebraic postexpressions recover a secret x, yielding a purely theoretical but fully worked semantic framework.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:05Weakest preconditions with weather forecast
- 5:19Quantitative reasoning and weakest preconditions
- 7:44Quantitative strongest post conditions
- 9:28Examples and rules for QSP
- 11:36Quantitative information flow
- 13:03Liberal vs non-liberal transformers
- 15:36Strongest liberal post conditions
- 17:22Galua connection between transformers
- 18:28Horror logic and incorrectness logic
- 21:01Eight combinations of transformers
- 22:07Question and answer session
related talks
30mRelatively Complete Verification of Probabilistic Programs
14mLOUD: Synthesizing Strongest and Weakest Specifications
16mInterpolation and Quantifiers in Ortholattices
49mSemantic Foundations for Probabilistic Programming
30mThe Verse Calculus: A Core Calculus for Deterministic Functional Logic Programmi...
29mHigher-Order Weakest Precondition Transformers via a CPS Transformation
22mA Calculus of Inductive Linear Constructions
18mQualifying System F-sub