Program Verification using Abductive Reasoning
summary
Uses abductive reasoning to synthesize loop invariants by asking what extra facts make the verification condition entail the postcondition, then checks inductiveness with an SMT solver. If a candidate is non‑inductive the system abduces auxiliary facts (e.g., strengthen to I≥1 and J≥−1) and backtracks/searches for alternatives, iterating until inductive or contradictory. Works on many real cases without user annotations but is not guaranteed to terminate and requires practical search limits.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 0:55What is your research area
- 2:45What is it about this area that you really like
- 3:45What is program verification
- 8:19Automating program verification
- 9:26Example
- 12:20Weakest Precondition
- 13:02Loop Invariant
- 14:43Mathematical Induction
- 16:21Code snippet
- 20:28Recap
- 24:07Simple Example
- 25:50Loop Invariants
- 30:13Abduction
- 36:16Summary
- 37:49Questions