Separation Logic for Higher-Order Store

12 years 1 months ago
Separation Logic for Higher-Order Store
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.
Bernhard Reus, Jan Schwinghammer
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Where CSL
Authors Bernhard Reus, Jan Schwinghammer
Comments (0)