Publication details

Saarland University Computer Science

Separation Logic for Higher-order Store

Bernhard Reus, Jan Schwinghammer

Computer Science Logic (CSL'06), Springer, September 2006

Separation Logic is a sub-structural logic that supports local reasoning for imperative programs. It is designed to elegantly describe sharing and aliasing properties of heap structures, thus facilitating the verification of programs with pointers. In past work, separation logic has been developed for heaps containing records of basic data types. Languages like C or ML, however, also permit the use of code pointers. The corresponding heap model is commonly referred to as higher-order store since heaps may contain commands which in turn are interpreted as partial functions between heaps.
In this paper we make Separation Logic and the benefits of local reasoning available to languages with higher-order store. In particular, we introduce an extension of the logic and prove it sound, including the Frame Rule that enables specifications of code to be extended by invariants on parts of the heap that are not accessed.

Download PDF        Show BibTeX               

Login to edit

Legal notice, Privacy policy