On an efficient decision procedure for imperative tree data structures

Wies, Thomas and Muñiz, Marco and Kuncak, Viktor (2011) On an efficient decision procedure for imperative tree data structures. Technical Report. IST Austria.

[img] Text
IST-2011-0005.pdf - Published Version
Available under License All rights reserved.
[IST-2011-0005]
Download (604Kb)

Abstract

We present a new decidable logic called TREX for expressing con- straints about imperative tree data structures. In particular, TREX supports a tran- sitive closure operator that can express reachability constraints, which often ap- pear in data structure invariants. We show that our logic is closed under weakest precondition computation, which enables its use for automated software verifica- tion. 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 tradi- tionally used for reasoning about tree data structures.

Item Type: Monograph (Technical Report)
DOI: IST-2011-0005
Subjects: 000 Computer science, knowledge & general works > 000 Computer science, knowledge & systems
000 Computer science, knowledge & general works > 000 Computer science, knowledge & systems > 006 Special computer methods
Research Group: Henzinger Group
Depositing User: Kate Longley
Date Deposited: 16 Jul 2012 08:37
Last Modified: 19 Sep 2017 15:17
URI: https://repository.ist.ac.at/id/eprint/19

Actions (login required)

View Item View Item