Decidable Logics Combining Heap Structures And Data

We define a new logic, STRAND, that allows reasoning with heap-manipulating programs using deductive verification and SMT solvers. STRAND logic :("STRucture ANd Data" logic) formulas express constraints involving heap structures and the data they contain; they are defined over a class of pointer-structures R defined using MSO-defined relations over trees, and are of the form there exists x ->for all(->)(y)phi((->)(x), (->)(y)), where phi is a monadic second-order logic (MSO) formula with addtional quantification that combines structural constraints as well as data-constraints, but where the data-constraints are only allowed to refer (->)(x) and (->)(y).The salient aspects of the logic are: (a) the logic is powerful, allowing existential and universal quantification over the nodes, and complex cambinatiens of data and structural constraints; (b) checking Hoarre-triples tor linear blocks of statements with preconditions and post-conditions expressed as Boolean combinations of existential and universal STRAND formulas reduces to satisfiability of a STRAND formula; (c) there are powerful decidable fragments of STRAND, one semantically defined and one syntactically defined, where the decision procedure works by combining the theory of MSO over crees and the quantifier-frez theory of the underlying data-logic. We: demonstrate the effectiveness and practicality of the: logic by checking verification conditions generated in proving properties of several heap-manipulating programs, using a tool that combines an MSO decision procedure over trees (MONA) with an SMT solver for integer constraints (Z3).