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.