Decidable logics combining heap structures and data

Abstract

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∀→y (→x,→) x" , where "φ" is a monadic second-order logic (MSO) formulawith 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"