** High Level Program Reasoning **

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.