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

  Browse A-Z

Log in

Cambridge users (raven)details Other usersdetails No account?details

Information on

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

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.

Other lists

Biophysical Colloquia Tackling Obesity with Big Data: methods & models - One Day Seminar Cavendish Knowledge Exchange Working Lunch Series Cambridge Analysts' Knowledge Exchange Marr Club One Day Workshop on: "The Greek language in Pontus: Romeyka in contemporary Trebizond"

Other talks

The persistence and transience of memory Structurally unravelling ATP synthase What sort of challenge is climate change? Fifty years of editorialising in ‘Nature’ and ‘Science’ Developing joint research between a UK university and and INGO on disability and education: opportunities and challenges Trees as keys, ladders, maps: a revisionist history of early systematic trees Protein Folding, Evolution and Interactions Symposium Single Cell Seminars (September) The Productivity Paradox: are we too busy to get anything done? Computing High Resolution Health(care) Cambridge - Corporate Finance Theory Symposium September 2017 - Day 1 SciScreen: Finding Dory
 

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