University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > The Relationship Between Separation Logic and Implicit Dynamic Frames

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

The Relationship Between Separation Logic and Implicit Dynamic Frames

Download to your calendar using vCal

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins .

This event may be recorded and made available internally or externally via http://research.microsoft.com. Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

Separation Logic is a popular approach to the formal verification of heap-manipulating programs. More recently, Implicit Dynamic Frames has been proposed as an alternative specification logic which is tailored for automatic verification based on state-of-the-art first-order solvers such as Z3 (cf. the Chalice and VeriCool tools). In this talk, I will present recent work (in collaboration with Matthew Parkinson) in formally connecting the two specification logics for the first time, and the resulting technical benefits that this yields for both approaches.

The work has been extended since our initial ESOP 2011 paper, to incorporate a novel semantics for the intuitionistic implication and magic wand connectives which works well for both approaches and could lead to better practical implementations of these (typically unsupported) connectives in future tools. I’ll also discuss some follow-on projects which have been influenced by this connection.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

The William Harvey Lecture Theatre, School of Cinical Medicine, Addenbrooke's Site 2S5 Donald McIntyre Building, Faculty of Education, 184 Hills Road, Cambridge Room GS15 at the William Gates Building and on Zoom: https://cl-cam-ac-uk.zoom.us/j/4361570789?pwd=Nkl2T3ZLaTZwRm05bzRTOUUxY3Q4QT09&from=addon

Other talks

Morning Tea and Coffee Title to be confirmed  Life, death, and the discovery of PDAR: the Pol II Degradation-dependent Apoptotic Response  Title to be confirmed Title TBC Title to be confirmed
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity