Abstract

Separation Logic is a substructural logic that supports local reasoning about imperative programs, in the sense that for the verification of program fragments only the reachable part of the heap must be taken into account. In past work, Separation Logic has been developed  for heaps containing records  of basic data types. Yet, languages like C or ML also allow procedures to be stored on the heap. The corresponding heap model is commonly referred to as "general storage" (or "higher-order store").

In this talk I will address the problem of lifting Separation Logic from first-order to higher-order store. To this end, we develop a Hoare-style logic featuring Separation Logic connectives for a simple imperative language with dynamic memory management and storable commands. To prove soundness, the language is endowed with a denotational semantics. As a benefit, we can reuse further powerful proof rules for programs using general storage.

This is joint work with Bernhard Reus, University of Sussex.