Executable Separation Logic Specifications in CN

Add to your list(s) Download to your calendar using vCal

• Rini Banerjee (University of Cambridge)
• Monday 04 November 2024, 13:00-14:00
• FS07, Computer Laboratory.

If you have a question about this talk, please contact Ariadne Si Suo .

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 .

This talk is part of the SANDWICH Seminar (Computer Laboratory) series.

This talk is included in these lists:

• FS07, Computer Laboratory
• tcw57’s list

Note that ex-directory lists are not shown.