Fulminate: Testing CN Separation-Logic Specifications in C

This conference talk presents research on Fulminate, a novel approach for testing CN separation-logic specifications in C through runtime verification. Learn how researchers from the University of Cambridge developed a system that translates separation logic specifications into executable runtime checks, addressing the challenge of evaluating separation-logic formulas during concrete execution. The presentation explores how a restricted fragment of separation logic used in the CN proof tool enables practical runtime testing with ownership checks and ownership transfer capabilities. Discover the implementation details of this C+CN source to C source translation tool and see demonstrations on complex examples, including an allocator from a production hypervisor. The talk covers the formalization of the runtime ownership testing scheme and proves how its reified ghost state correctly captures ownership passing in a C-like language semantics. Valuable for researchers and developers interested in program verification, separation logic, refinement types, and runtime testing for systems programming languages.