Local Hoare Reasoning about DOM
Philippa Gardner
Abstract: In this talk, I will describe local Hoare reasoning about the Document Object Model (DOM), a W3C XML update library which views XML as an in-place memory store rather than a static XML document. Our work transfers O'Hearn, Reynolds and Yang's local Hoare reasoning for analysing heap update using Separation Logic to XML update. In particular, we apply recent work by Calcagno, Gardner and Zarfaty on local Hoare reasoning about simple tree update using Context Logic to DOM. We provide a formal, compositional specification of DOM. Unlike DOM, we are able to work with a minimal set of commands and obtain a complete reasoning for straight-line code. Our reasoning not only formally specifies a significant subset of DOM Core Level 1, but can also be used to verify, for example, invariant properties of simple Javascript programs.
This talk is based on joint work with Gareth Smith, Mark Wheelhouse and Uri Zarfaty.
Bio: Dr Philippa Gardner is a Reader in the Department of Computing at Imperial, and a Microsoft Research Cambridge/Royal Academy of Engineering Senior Research Fellow. Her current research centres on local Hoare reasoning about structured data update, process calculi for analysing features of distributed systems, and languages for manipulating web data. She obtained her PhD on type theory and logical frameworks at Edinburgh, supervised by Professor Gordon Plotkin. She held a SERC Postdoctoral Fellow and a Royal Society of Edinburgh BP Fellow at Edinburgh, and an EPSRC Advanced Fellow at Cambridge and Imperial. She has been at Imperial since 2000.