An efficient decision procedure for imperative tree data structures

Thomas Wies; Marco Muñiz; Viktor Kuncak

doi:10.1007/978-3-642-22438-6_36

An efficient decision procedure for imperative tree data structures

Thomas Wies, Marco Muñiz, Viktor Kuncak

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English (US)
Title of host publication	Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Proceedings
Pages	476-491
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-22438-6_36
State	Published - 2011
Event	23rd International Conference on Automated Deduction, CADE 23 - Wroclaw, Poland Duration: Jul 31 2011 → Aug 5 2011

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	6803 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	23rd International Conference on Automated Deduction, CADE 23
Country/Territory	Poland
City	Wroclaw
Period	7/31/11 → 8/5/11

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-642-22438-6_36

Cite this

Wies, T., Muñiz, M., & Kuncak, V. (2011). An efficient decision procedure for imperative tree data structures. In Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Proceedings (pp. 476-491). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6803 LNAI). https://doi.org/10.1007/978-3-642-22438-6_36

An efficient decision procedure for imperative tree data structures. / Wies, Thomas; Muñiz, Marco; Kuncak, Viktor.
Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Proceedings. 2011. p. 476-491 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6803 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Wies, T, Muñiz, M & Kuncak, V 2011, An efficient decision procedure for imperative tree data structures. in Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6803 LNAI, pp. 476-491, 23rd International Conference on Automated Deduction, CADE 23, Wroclaw, Poland, 7/31/11. https://doi.org/10.1007/978-3-642-22438-6_36

Wies T, Muñiz M, Kuncak V. An efficient decision procedure for imperative tree data structures. In Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Proceedings. 2011. p. 476-491. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-22438-6_36

Wies, Thomas ; Muñiz, Marco ; Kuncak, Viktor. / An efficient decision procedure for imperative tree data structures. Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Proceedings. 2011. pp. 476-491 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{94b6047cbb564f20ae3024d605066599,

title = "An efficient decision procedure for imperative tree data structures",

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.",

author = "Thomas Wies and Marco Mu{\~n}iz and Viktor Kuncak",

year = "2011",

doi = "10.1007/978-3-642-22438-6_36",

language = "English (US)",

isbn = "9783642224379",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "476--491",

booktitle = "Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Proceedings",

note = "23rd International Conference on Automated Deduction, CADE 23 ; Conference date: 31-07-2011 Through 05-08-2011",

}

TY - GEN

T1 - An efficient decision procedure for imperative tree data structures

AU - Wies, Thomas

AU - Muñiz, Marco

AU - Kuncak, Viktor

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=80051690412&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=80051690412&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-22438-6_36

DO - 10.1007/978-3-642-22438-6_36

M3 - Conference contribution

AN - SCOPUS:80051690412

SN - 9783642224379

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 476

EP - 491

BT - Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Proceedings

T2 - 23rd International Conference on Automated Deduction, CADE 23

Y2 - 31 July 2011 through 5 August 2011

ER -

An efficient decision procedure for imperative tree data structures

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this