An efficient decision procedure for imperative tree data structures

DOI10.1007/978-3-642-22438-6_36MaRDI QIDQ5200043zbMATH OpenOpenAlexFDO

Authors Thomas Wies, Marco Muñiz, Viktor Kuncak

Publication date 29 July 2011

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://repository.ist.ac.at/19/1/IST-2011-0005.pdf

Mathematics Subject Classification ID

Logic in computer science (03B70) Data structures (68P05)

Recommendations

• A decidable logic for tree data-structures with measurements
• Satisfiability of compositional separation logic with tree predicates and data constraints
• Reasoning About Data Trees Using CHCs
• Recursive proofs for inductive tree data-structures
• Building a calculus of data structures

Cites work

• A logic of reachable patterns in linked data-structures
• A Logic-Based Framework for Reasoning about Composite Data Structures
• Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
• An efficient decision procedure for imperative tree data structures
• Automata-based verification of programs with tree updates
• Automated Deduction – CADE-20
• Automated Deduction – CADE-20
• Back to the future, revisiting precise program verification using SMT solvers
• Computer Science Logic
• Counterexample-guided focus
• On Local Reasoning in Verification
• On the complexity of the Bernays-Schönfinkel class with Datalog
• Reasoning in expressive description logics
• Shape Analysis of Single-Parent Heaps
• Verification, Model Checking, and Abstract Interpretation

Cited in

(10)

• Nested antichains for WS1S
• Controlling the data space of tree structured computations
• A decidable logic for tree data-structures with measurements
• Lazy automata techniques for WS1S
• Local reasoning for global graph properties
• An efficient decision procedure for imperative tree data structures
• Complete instantiation-based interpolation
• Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure
• Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure
• Antiprenexing for WSkS: a little goes a long way

Describes a project that uses

Uses Software

• z3
• MONA

This page was built for publication: An efficient decision procedure for imperative tree data structures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5200043)