Fulminate: Testing CN Separation-Logic Specifications in C
summary
Fulminate translates CN separation-logic annotations into executable C checks that enforce ownership ghost state and explicit ownership transfer at runtime, with a proved semantics that the reified ghost state matches CN’s resource passing. The prototype inserts assertions into C, compiles and runs; applied to a pKVM buddy allocator (about 300 LOC C / 700 LOC CN) and completes translation+build+run in ~30 seconds. Current limits: sequential-only ghost-state tracking, basic allocation without GC, and no automated test-case generation.
AI-written summary · about
chapters (10)
- 0:00Fulminate introduction
- 1:04Full functional correctness challenges
- 2:48Test specs instead of proving
- 4:34CN separation logic in C
- 6:03How CN separation logic works
- 8:33Transforming specs to assertions
- 9:16Dynamic ownership checking
- 11:43Fulminate for hypervisor code
- 13:27Summary and future
- 13:54Q&A on testing
related talks
45mFil-C: memory safety with fanatical C/C++ compatibility
29mSecuring C code that seems to work just fine
59mTheory makes beautiful programs
01h 03mCLANG + C2 - Engineering/Futures/Measurements
56mSpectre/C++
01h 38mZero-allocation & no type erasure futures
01h 16mPolymorphism, Cohesion, and Coupling in C++
18mMix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations