Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq
summary
Quiver claims automated inference of full separation logic specs for C code while verifying soundness in Coq using Iris, implemented as a prototype atop RefineC and producing predicate Transformer specifications. It fills user-provided sketches by running a new abductive deductive verification engine, reconstructs library-derived specs, and handles pointer arithmetic, malloc, memcopy, and conditionals. Evaluation includes multiple case studies and a reusable artifact archive; limitations include no inferred loop invariants, no predicate synthesis, and limited C feature support.
AI-written summary · about
chapters (9)
- 0:00Quiver introduction
- 1:45Guided spec inference
- 2:50Refined C limitations
- 4:14Abduction restrictions
- 5:39Three-step inference
- 7:25Deductive verification
- 12:40Scaling with growth
- 14:24Quiver limitations
- 15:08Q&A
related talks
46mMechanizing Abstract Interpretation
01h 34mFormal Logic Undressed
19mBeyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
25mA Relational Separation Logic for Effect Handlers
21mCompositional pre-processing for automated reasoning in dependent type theory
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
23mVellvm: Formalizing the Informal