TY - GEN

T1 - Decidable logics combining heap structures and data

AU - Madhusudan, P.

AU - Parlato, Gennaro

AU - Qiu, Xiaokang

N1 - Copyright:
Copyright 2011 Elsevier B.V., All rights reserved.

PY - 2010

Y1 - 2010

N2 - 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 ℛ 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 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 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).

AB - 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 ℛ 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 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 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).

KW - Automata

KW - Combining decision procedures

KW - Decidability

KW - Heap analysis

KW - Monadic second-order logic

KW - SMT solvers

UR - http://www.scopus.com/inward/record.url?scp=79952016328&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=79952016328&partnerID=8YFLogxK

U2 - 10.1145/1926385.1926455

DO - 10.1145/1926385.1926455

M3 - Conference contribution

AN - SCOPUS:79952016328

SN - 9781450304900

T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages

SP - 611

EP - 622

BT - POPL'11 - Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

T2 - 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'11

Y2 - 26 January 2011 through 28 January 2011

ER -