An efficient decision procedure for imperative tree data structures

Thomas Wies, Marco Muñiz, Viktor Kuncak

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish (US)
Title of host publicationAutomated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Proceedings
Pages476-491
Number of pages16
Volume6803 LNAI
DOIs
StatePublished - 2011
Event23rd International Conference on Automated Deduction, CADE 23 - Wroclaw, Poland
Duration: Jul 31 2011Aug 5 2011

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6803 LNAI
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other23rd International Conference on Automated Deduction, CADE 23
CountryPoland
CityWroclaw
Period7/31/118/5/11

Fingerprint

Decision Procedures
Tree Structure
Data structures
Data Structures
Logic
Monadic Second-order Logic
Software Verification
Transitive Closure
Closure Operator
Precondition
Reachability
Low Complexity
Express
Reasoning
Closed
Invariant
Alternatives

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

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 (Vol. 6803 LNAI, 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. Vol. 6803 LNAI 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 proceedingConference 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. vol. 6803 LNAI, 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. Vol. 6803 LNAI. 2011. p. 476-491. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/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. Vol. 6803 LNAI 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",
volume = "6803 LNAI",
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",

}

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

VL - 6803 LNAI

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

ER -