Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…)
summary
Integrates CN separation logic into runtime checks, unit and SMT-based random generator testing, and final machine-checked proofs, all on the real-world PKVM heap allocator running bare-metal; instrumentation handles huge preprocessed C, supports ghost args, and generates heap shapes from specs. Results: the workflow finds 20 specification bugs and 4 implementation bugs (all fixed), and achieves full verification of malloc/free retroactively with minimal C changes; artifacts and code are available.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 0:27Formal verification in C
- 1:09All-or-nothing verification
- 1:31Incremental workflow
- 2:13Specify-test-debug cycle
- 2:54Toolchain and CN logic
- 3:35Technical contributions
- 4:18PKVM heap allocator case study
- 5:45Chunk install iteration
- 6:46Runtime spec checking
- 7:27Debugging specs conventionally
- 8:28Refining specs via debugging
- 9:10Bare metal spec testing
- 10:34Random testing from specs
- 12:00Moving to proof
- 13:06PKVM results
- 14:09Conclusion
- 15:23Q&A
related talks
28mGradual Verification: Assuring Software Incrementally
20mAutomatic and Incremental Repair for Speculative Information Leaks
15mGradual Verification of Recursive Heap Data Structures
22mImplementing separation logic using an SMT-backed Frame Rule
19mPete's Footprints
19mPredictable Verification using Intrinsic Definitions
13mA Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs
01h 07mThe seL4 verification: the art and craft of proof and the reality of commercial s