Decidable logics combining heap structures and data

We define a new logic, STRAND, that allows reasoning with heapmanipulating 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∀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 redu...

• Type: Journal
• Year: 2011
• Where: POPL
• Authors: P. Madhusudan, Gennaro Parlato, Xiaokang Qiu
• Keywords: Decidable Fragments, Integer Constraints, Pointer Structures, POPL 2011, Programming Languages