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

The Relationship Between Separation Logic and Implicit Dynamic Frames

Add to your list(s) 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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

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