Data structure specifications via local equality axioms

Abstract

We describe a program verification methodology for specifying global shape properties of data structures by means of axioms involving predicates on scalar fields, pointer equalities, and pointer disequalities, in the neighborhood of a memory cell. We show that such local invariants are both natural and sufficient for describing a large class of data structures. We describe a complete decision procedure for axioms without disequalities, and practical heuristics for the full language. The procedure has the key advantage that it can be extended easily with reasoning for any decidable theory of scalar fields. © Springer-Verlag Berlin Heidelberg 2005.