Sciweavers

Share
POPL
2011
ACM

Decidable logics combining heap structures and data

8 years 1 months ago
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...
P. Madhusudan, Gennaro Parlato, Xiaokang Qiu
Added 17 Sep 2011
Updated 17 Sep 2011
Type Journal
Year 2011
Where POPL
Authors P. Madhusudan, Gennaro Parlato, Xiaokang Qiu
Comments (0)
books