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( Ε)x~→(A)y~→Φ(x~→, y~→), where Φ is a monadic second-order logic (MSO) formula with additional quantification that combines structural constraints as well as data-constraints, but where the data-constraints are only allowed to refer to 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 combinations of data and structural constraints: (b) checking Hoare-triples for 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 semanticaily defined and one syntactically defined, where the decision procedure works by combining the theory of MSO over trees and the quantifier-free 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).