Earlier Version

On an efficient decision procedure for imperative tree data structures

Wies T, Muñiz M, Kuncak V. 2011. On an efficient decision procedure for imperative tree data structures, IST Austria, 25p.

Download
OA IST-2011-0005_IST-2011-0005.pdf 619.05 KB [Published Version]

Technical Report | Published | English
Author
Wies, ThomasISTA; Muñiz, Marco; Kuncak, Viktor
Series Title
IST Austria Technical Report
Abstract
We present a new decidable logic called TREX for expressing constraints about imperative tree data structures. In particular, TREX supports a transitive closure operator that can express reachability constraints, which often appear in data structure invariants. We show that our logic is closed under weakest precondition computation, which enables its use for automated software verification. We further show that satisfiability of formulas in TREX is decidable in NP. The low complexity makes it an attractive alternative to more expensive logics such as monadic second-order logic (MSOL) over trees, which have been traditionally used for reasoning about tree data structures.
Publishing Year
Date Published
2011-04-26
Page
25
ISSN
IST-REx-ID

Cite this

Wies T, Muñiz M, Kuncak V. On an Efficient Decision Procedure for Imperative Tree Data Structures. IST Austria; 2011. doi:10.15479/AT:IST-2011-0005
Wies, T., Muñiz, M., & Kuncak, V. (2011). On an efficient decision procedure for imperative tree data structures. IST Austria. https://doi.org/10.15479/AT:IST-2011-0005
Wies, Thomas, Marco Muñiz, and Viktor Kuncak. On an Efficient Decision Procedure for Imperative Tree Data Structures. IST Austria, 2011. https://doi.org/10.15479/AT:IST-2011-0005.
T. Wies, M. Muñiz, and V. Kuncak, On an efficient decision procedure for imperative tree data structures. IST Austria, 2011.
Wies T, Muñiz M, Kuncak V. 2011. On an efficient decision procedure for imperative tree data structures, IST Austria, 25p.
Wies, Thomas, et al. On an Efficient Decision Procedure for Imperative Tree Data Structures. IST Austria, 2011, doi:10.15479/AT:IST-2011-0005.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]
Main File(s)
Access Level
OA Open Access
Date Uploaded
2018-12-12
MD5 Checksum
b20029184c4a819c5f4466a4a3d238b5


Export

Marked Publications

Open Data ISTA Research Explorer

Search this title in

Google Scholar