Partial Incorrectness Logic
summary
Defines "partial incorrectness" as an underapproximation of the strongest liberal postcondition that admits final states that are provably unreachable, establishing a formal dual to partial correctness via Dijkstra-style predicate transformers. Shows Park induction makes lower-bound proofs on greatest fixpoints easier, separates reachability proofs from incorrectness proofs, and uses a concrete branch example (y+1 vs y*2) to show which poststates are unreachable rather than just absent from the precondition. Suggests a quantitative extension and tooling directions.
AI-written summary · about
chapters (9)
- 0:00Partial Incorrectness Logic
- 1:05Total to partial correctness
- 2:50Weakest preconditions and fixpoints
- 4:16Correctness versus incorrectness
- 5:41Strongest postconditions
- 8:10Example of partial incorrectness
- 10:38Necessary preconditions
- 12:26Summary and ongoing work
- 13:53Q&A
related talks
30mRelatively Complete Verification of Probabilistic Programs
25mA Logic for the Imprecision of Abstract Interpretations
17mFormalizing Determinacy of Concurrent Revisions
15mTowards a Unified Proof Framework for Automated Fixpoint Reasoning using Matching Logic
19mSimplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
17mA Better Approximation for Interleaved Dyck Reachability
32mA mechanised and constructive reverse analysis of soundness and completeness of b...
24mThe Best of Abstract Interpretations