Local Resource Reasoning about Program Modules such as DOM

Philippa Gardner ( Imperial College London )

Local resource reasoning provides modular reasoning about programs,based on the analysis of a program’s use of resource. This style of reasoning was first introduced in Separation Logic, a program logic for reasoning about C-programs. Separation Logic was extended with abstract predicates to provide course-grained reasoning about program modules, and generalised to Context Logic to provide fine-grained reasoning about program modules.

In this talk, I will describe recent work on fine-grained reasoning about program modules, using the W3C XML update library DOM as the running example. In particular, I will present an axiomatic specification of DOM using Context Logic, and verify DOM implementations by introducing locality-preserving and locality-breaking translations between the abstract DOM specification and the concrete implementations.

I will conclude by describing two on-going projects arising from this work: work on fine-grained reasoning about concurrent modules using concurrent abstract predicates with Dodds, Parkinson and Vafeiadis at Cambridge; and work on local reasoning about client-side web programming (DOM/Javascript) with Maffeis at Imperial.