BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Executable Separation Logic Specifications in CN - Rini Banerjee (
 University of Cambridge)
DTSTART:20241104T130000Z
DTEND:20241104T140000Z
UID:TALK223507@talks.cam.ac.uk
CONTACT:Ariadne Si Suo
DESCRIPTION:C is everywhere\, whether we like it or not. By allowing progr
 ammers to manually manage memory with complicated ownership patterns\, it
 ’s ideal for low-level programming but not so ideal for those who want t
 o 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]). Howeve
 r\, little work has been done on testing separation logic specifications i
 n 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.\n\n[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.
LOCATION:FS07\, Computer Laboratory
END:VEVENT
END:VCALENDAR