Memory-Safety Verification of Open Programs With Angelic Assumptions
summary
Seeker automatically suppresses spurious memory-safety warnings in open C programs by mining 1,900+ buffer idioms from an LLM, collapsing them into seven assumption templates, and using property-directed synthesis (weakest preconditions) to instantiate angelic assumptions that make counterexamples unrealizable. It iterates verify → synthesize → reverify, producing concrete assumptions such as null-terminated src and destination length == n, labels remaining failures as true bugs, and on 182 benchmarks suppresses ~79% of false positives with zero false negatives.
AI-written summary · about
chapters (8)
- 0:00Memory safety verification intro
- 1:26Demonic behavior in open programs
- 2:29Angelic assumptions goal
- 3:11LLM for idiomatic patterns
- 4:38Seven assumption templates
- 5:42Synthesizing angelic assumptions
- 8:09Evaluation on 182 benchmarks
- 9:55Q&A
related talks
01h 00mAI Safety through Programming?
28mProving Memory Access Violations in Isabelle/HOL
26mVerification of Programs with Concealed Components
28mMemory simulations, security and optimization in a verified compiler
01h 06mmemory-safe C++
43mEverything I learned about static analysis and program safety in C++
29müberSpark: Enforcing Verifiable Object Abstractions for Automated...
17mProving capability safety in the presence of indirect sentries