An Efficient Decision Procedure for Imperative Tree Data Structures
From MaRDI portal
Publication:5200043
DOI10.1007/978-3-642-22438-6_36zbMath1341.68034MaRDI QIDQ5200043
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
Related Items
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, Nested antichains for WS1S, Lazy Automata Techniques for WS1S
Uses Software
Cites Work
- Unnamed Item
- Automata-based verification of programs with tree updates
- A logic of reachable patterns in linked data-structures
- A Logic-Based Framework for Reasoning about Composite Data Structures
- Back to the future
- Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
- On the Complexity of the Bernays-Schönfinkel Class with Datalog
- An Efficient Decision Procedure for Imperative Tree Data Structures
- Counterexample-guided focus
- Computer Science Logic
- Automated Deduction – CADE-20
- Automated Deduction – CADE-20
- Shape Analysis of Single-Parent Heaps
- On Local Reasoning in Verification
- Verification, Model Checking, and Abstract Interpretation
