A Comparison of Program Logics for (In)Correctness
summary
Compares program logics by exact approximation direction and shows over/under duality breaks: Hoare-style correctness and necessary-precondition triples map tightly, but incorrectness logic and the new Sufficient Incorrectness Logic (SIL) give no general correspondence. Proposes sound and complete proof system for the backward under-approximation condition with five core rules (backward loop unrolling, choice, consequence variants), instantiates it as Separation SIL for heaps, proves completeness on concrete semantics and presents a vector-reallocation example where Separation SIL yields stronger, usable bug witnesses.
AI-written summary · about
chapters (9)
- 0:00Program logics for correctness
- 1:27Fixing notation and semantics
- 3:13Correctness vs incorrectness logics
- 7:07Logics along approximation axis
- 9:16Sufficient incorrectness proof system
- 14:12Core rules and backward analysis
- 15:39Instantiating with separation logic
- 19:32Future directions for logics
- 21:42Q&A
related talks
42mQuantum program analysis: Verification and Testing
19mNon-Termination Proving at Scale
59mUnder-approximation for Scalable Bug Detection
37mContracts For Getting More Programs Less Wrong
01h 09mLocknote: Local Reasoning in C++
22mHypra: A Deductive Program Verifier for Hyper Hoare Logic
51mWhen Types are Not Enough
18mPreview: Verification (Correctness)