Verifying Infinitely Many Programs at Once
summary
Proposes proving unrealizability for entire program search spaces by reducing synthesis-to-verification and by designing a Hoare-like logic that reasons about sets of programs. Builds three concrete pipelines: a reachability encoding using Seahorn, a precise grammar-flow analysis for expression grammars (a decidable fragment over linear integer arithmetic and examples), and CHC encodings solved with Spacer (and Vampire for infinite-array reasoning). Ships tools that solve new benchmarks, proves about half of imperative cases, and produces novel invariants describing properties of infinitely many programs.
AI-written summary · about
chapters (10)
- 0:00Verifying infinitely many programs
- 5:24Failed synthesis to new research
- 10:40Synthesis via verification
- 17:24Grammar flow analysis
- 24:34From expressions to imperative
- 31:40Shifting sands problem
- 38:39Infinite program invariants
- 46:48Unrealizability logic
- 52:46Applications and future
- 1:02:20Q&A on type systems
related talks
27mUnrealizability Logic
20mAutomating Unrealizability Logic: Hoare-style Proof Synthesis for Infinite Sets of(…)
52mThink Abstractly, Work Concretely
12mFO-Complete Program Verification for Heap Logics
24mProving False in Object Oriented Verification Programs by Exploiting Non-Termination
47mHow to trust a verified program?
23mSpecifying and Verifying Future Conditions
22mProgram Synthesis for Artifacts beyond Programs