Backward Symbolic Execution with Loop Folding
summary
Presents backward symbolic execution with loop folding that proves error unreachability by deriving inductive, often disjunctive loop invariants from backward states instead of unwinding loops; formalizes that bounded backward execution implements k‑induction (k → k−1). Implements BSELF and runs it on 770 SV‑COMP loops benchmarks: BSELF verifies several standard benchmarks that state‑of‑the‑art tools miss, solves more non‑trivial cases overall, with a few solved only by plain backward execution and many solved only by BSELF.
AI-written summary · about
chapters (9)
- 0:00Outline
- 0:33Control Flow Automata (CFA)
- 1:05Symbolic Execution (SE)
- 3:13Backward Symbolic Execution (BSE)
- 5:06K-Induction on CFAs
- 6:28BSE and K-Induction
- 7:12BSE with Loop Folding (BSELF)
- 10:48Evaluation - BSE vs. BSELF
- 11:40Evaluation - BSELF vs. the world
related talks
13mRevealing Sources of (Memory) Errors via Backward Analysis
24mU-Turn: Enhancing Incorrectness Analysis by Reversing Direction
21mExact Loop Bound Analysis
20mOn Extending Incorrectness Logic with Backwards Reasoning
26mUnfolding Expressions for Gradual Verification
24mQSYM : A Practical Concolic Execution Engine Tailored for Hybrid Fuzzing
24mSymbiotic: finding bugs in C programs
24mProving False in Object Oriented Verification Programs by Exploiting Non-Termination