A decidable class of verification conditions for programs with higher order store

Abstract

Recent years have seen a surge in techniques and tools for automatic and semi-automatic static checking of imperative heap-manipulating programs. At the heart of such tools are algorithms for automatic logical reasoning, using heap description formalisms such as separation logic. In this paper we work towards extending these static checking techniques to languages with procedures as first class citizens. To do this, we first identify a class of entailment problems which arise naturally as verification conditions during the static checking of higher order heap-manipulating programs. We then present a decision procedure for this class and prove its correctness. Entailments in our class combine simple symbolic heaps, which are descriptions of the heap using a subset of separation logic, with (limited use of) nested Hoare triples to specify properties of higher order procedures.