Indexes - also known as associative arrays, dictionaries, maps, or hashes - are abstract data-structures with myriad applications, from databases to dynamic languages. Abstractly, an index is a partial function from keys to values. Values can be queried by their keys, and the index can be mutated by adding or removing mappings. While appealingly simple, this abstract view is insufficient for reasoning about indexes that are accessed concurrently.

In this paper, we introduce an abstract specification which views an index as a divisible resource. Multiple threads can access the index concurrently, yet threads can still reason locally. We show that this specification can be used to verify a number of client applications. Our abstract specification would mean little if it were not satisfied by the implementations of concurrent indexes. We verify that our specification is satisfied by linked list, hash table and B-Link tree index implementations. During verification, we uncovered a subtle bug in the B-Link tree algorithm.

Separation Logic (O'Hearn et al.) provides local reasoning about programs that manipulate a low-level heap. Not only has it been used with great success to reason about sequential programs, but it has also been extended, in a variety of ways, to reason about programs with concurrent behaviour, whilst still adhering to the ideals of local reasoning.

Context Logic (Gardner et al.) was introduced to generalise the ideas of Separation Logic to higher levels of data abstraction. This has most notably been used to provide a local, formal and compositional version of the W3C DOM specification. However, the concept of splitting program data into a context and some sub-data does not extend well to the concurrent setting.

We have recently introduced Segment Logic to provide a more fine-grained notion of splitting up program data at the high level. We shall introduce Segment Logic and show how the low-level concurrency rules from Separation Logic can be interpreted at the high-level.

O'Hearn, Reynolds and Yang introduced Separation Logic to provide modular reasoning about simple, mutable data structures in memory. They were able to construct small specifications of programs by reasoning about the local parts of memory accessed by programs (their footprints). They have used their Low-Level reasoning to notable success verifying memory safety properties of C programs and device drivers.

Gardener, Calcagno and Zarfaty have generalised this work, introducing Context Logic to reason about more complex, High-Level, data structures in order to reason at the level of the program abstraction. In particular, with Smith and Wheelhouse, they have developed a formal, compositional specification for the Document Object Model (DOM) a W3C XML update library. However, whilst keeping to the spirit of local reasoning, they were not able to retain small specifications for all of their update commands.

We have since introduced Segment Logic, which provides a more fine-grained analysis of data structures and yields small specifications for all of our update commands. As well as being aesthetically pleasing, small specifications are essential for reasoning about concurrent update programs.

In this survey talk we shall take a look at the progression of program verification from Low-Lewel to High-Level reasoning. We will begin with a quick look at Separation Logic before introducing Context Logic and showing how this enables us to specify the High-Level DOM commands without needing to know how they are implemented at the Low-Level. We shall then see how these specifications are unsuitable for reasoning about a concurrent XML update language, and look at how Segment Logic can be used to provide a more fine-grained specification of these commands that can be used in a concurrent setting.

O'Hearn, Reynolds and Yang introduced local Hoare reasoning about mutable data structures using Separation Logic. They reason about the local parts of the memory accessed by programs, and thus construct their smallest complete specifications. Gardner et al. generalised their work, using Context Logic to reason about structured data at the same level of abstraction as the data itself. In particular, they developed a formal specification of the Document Object Model, a W3C XML update library. Whilst they kept to the spirit of local reasoning, they were not able to retain small specifications: for example, the specification of appendChild was not small. We show how to obtain small specifications by working with a more fine-grained context structure, allowing us to work with arbitrary tree fragments.

We look at the problems of providing a small axiom for the append command in DOM. We concentrate on what is required to solve this problem and introduce a new logic that is able to describe high level data structures in a more fine-grained way.

A Presentation given to sixth form students in East London to outline what it means to be studying for a PhD. Gives a high-level overview of the topic of program reasoning and why it is important. Uses the idea of updating a family tree to explain the concept of local reasoning.

Hoare Logic allows us to reason about programs that alter data structures. We will look at two spatial logics that allow this reasoning to be carried out in a local fashion by providing command specifications in terms of 'Small Axioms', each of which mentions only the parts of the data structure accessed by that particular command.

The first of these is Separation Logic, which works with a low level storage system based on a C like heap structure. Separation Logic has been used very successfully in the testing of windows device drivers.

The second logic we shall consider is Context Logic which lets us reason about structured data update at a higher level of abstraction. Context Logic is currently being used to provide a formal specification for the DOM (Document Object Model) XML update library.

This talk is intended to provide an overview of these logics and identify some of the areas of interest that are currently under investigation.

An overview of my 4th year project on verifying DOM. Includes an introduction to the Minimal DOM data structure (later renamed Featherweight DOM) and Context Logic reasoning over this structure.