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

摘要

Recent years have seen a surge in techniques and tools for automatic andsemi-automatic static checking of imperative heap-manipulating programs. At theheart of such tools are algorithms for automatic logical reasoning, using heapdescription formalisms such as separation logic. In this paper we work towardsextending these static checking techniques to languages with procedures as firstclass 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 procedurefor this class and prove its correctness. Entailments in our class combinesimple symbolic heaps, which are descriptions of the heap using a subset ofseparation logic, with (limited use of) nested Hoare triples to specifyproperties of higher order procedures.