| Skip to main content | Skip to sub navigation |

This is now an inactive research group it's members have moved on. You can find them at their new research groups:

Speaker(s): Dr Philippa Gardner
Organiser: Dr Nicholas Gibbins
Time: 25/06/2007 13:00-14:00
Location: B32/3077

Abstract

There has been a recent breakthrough in Hoare reasoning. Researchers previously used Hoare reasoning based on First-order Logic to specify how programs interacted with the whole memory. O'Hearn, Reynolds and Yang instead introduced local Hoare reasoning based on Separation Logic. The key idea is to specify how programs interact with the small, local part of the memory (the footprint) touched by a program. Their work is proving to be essential for modular reasoning about large programs, and for reasoning about modern applications involving concurrent, distributed programming.

Inspired by this work, Calcagno, Gardner and Zarfaty studied local Hoare reasoning about XML update. We initially assumed that we could base our reasoning on Cardelli and Gordon's Ambient Logic, which analyses static trees (firewalls, XML) in a similar way to O'Hearn's analysis of heaps. In fact, we proved that this is not possible. Instead, we had to fundamentally change the way we reason about structured data, by introducing Context Logic for reasoning about both data and contexts.

In this talk, I will give an overview of local Hoare reasoning about XML update, based on Context Logic. This talk will be aimed at a general audience. I gather that Peter O'Hearn has recently given a talk on a verification tool based on Separation Logic. I will not assume knowledge of Separation Logic, but I hope that you will understand the connections between our work from my talk.

Presentation Links

Philippa Gardner's homepage

Speaker Biography

Dr Philippa Gardner

Philippa Gardner is a Reader at Imperial College, and holds a five-year senior research fellowship sponsored by Microsoft Research Cambridge and the Royal Academy of Engineering. Her current research spans programming language design, process models and web languages. She completed her Ph.D at Edinburgh in 1992 on type theory and logical frameworks, supervised by Gordon Plotkin, and has held several additional fellowships,including an EPSRC Advanced Fellowship at Cambridge University and Imperial College.