---
_id: '5383'
abstract:
- lang: eng
text: 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.
alternative_title:
- IST Austria Technical Report
author:
- first_name: Thomas
full_name: Wies, Thomas
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Marco
full_name: Muñiz, Marco
last_name: Muñiz
- first_name: Viktor
full_name: Kuncak, Viktor
last_name: Kuncak
citation:
ama: 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
apa: 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
chicago: 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.
ieee: T. Wies, M. Muñiz, and V. Kuncak, On an efficient decision procedure for
imperative tree data structures. IST Austria, 2011.
ista: Wies T, Muñiz M, Kuncak V. 2011. On an efficient decision procedure for imperative
tree data structures, IST Austria, 25p.
mla: Wies, Thomas, et al. On an Efficient Decision Procedure for Imperative Tree
Data Structures. IST Austria, 2011, doi:10.15479/AT:IST-2011-0005.
short: T. Wies, M. Muñiz, V. Kuncak, On an Efficient Decision Procedure for Imperative
Tree Data Structures, IST Austria, 2011.
date_created: 2018-12-12T11:39:01Z
date_published: 2011-04-26T00:00:00Z
date_updated: 2023-02-23T11:22:16Z
day: '26'
ddc:
- '000'
- '006'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2011-0005
file:
- access_level: open_access
checksum: b20029184c4a819c5f4466a4a3d238b5
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:01Z
date_updated: 2020-07-14T12:46:40Z
file_id: '5462'
file_name: IST-2011-0005_IST-2011-0005.pdf
file_size: 619053
relation: main_file
file_date_updated: 2020-07-14T12:46:40Z
has_accepted_license: '1'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: '25'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '19'
related_material:
record:
- id: '3323'
relation: later_version
status: public
status: public
title: On an efficient decision procedure for imperative tree data structures
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...