Abstract

C is everywhere, whether we like it or not. By allowing programmers to manually manage memory with complicated ownership patterns, it’s ideal for low-level programming but not so ideal for those who want to reason about these behaviours. Separation logic has become an important tool for capturing and reasoning about these ownership patterns, forming the basis of several static analysis and proof tools (e.g. CN [1]). However, little work has been done on testing separation logic specifications in concrete execution since at first glance, separation-logic formulas are hard to evaluate in a reasonable amount of time. In this talk I describe our work on Fulminate, a tool for executing CN specifications on concrete inputs in C.

[1] https://www.cl.cam.ac.uk/~nk480/cn.pdf, Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, Neel Krishnaswami. POPL 2023 .