--- _id: '3323' 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: - 'LNAI ' 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. An efficient decision procedure for imperative tree data structures. In: Vol 6803. Springer; 2011:476-491. doi:10.1007/978-3-642-22438-6_36' apa: 'Wies, T., Muñiz, M., & Kuncak, V. (2011). An efficient decision procedure for imperative tree data structures (Vol. 6803, pp. 476–491). Presented at the CADE 23: Automated Deduction , Wrocław, Poland: Springer. https://doi.org/10.1007/978-3-642-22438-6_36' chicago: Wies, Thomas, Marco Muñiz, and Viktor Kuncak. “An Efficient Decision Procedure for Imperative Tree Data Structures,” 6803:476–91. Springer, 2011. https://doi.org/10.1007/978-3-642-22438-6_36. ieee: 'T. Wies, M. Muñiz, and V. Kuncak, “An efficient decision procedure for imperative tree data structures,” presented at the CADE 23: Automated Deduction , Wrocław, Poland, 2011, vol. 6803, pp. 476–491.' ista: 'Wies T, Muñiz M, Kuncak V. 2011. An efficient decision procedure for imperative tree data structures. CADE 23: Automated Deduction , LNAI , vol. 6803, 476–491.' mla: Wies, Thomas, et al. An Efficient Decision Procedure for Imperative Tree Data Structures. Vol. 6803, Springer, 2011, pp. 476–91, doi:10.1007/978-3-642-22438-6_36. short: T. Wies, M. Muñiz, V. Kuncak, in:, Springer, 2011, pp. 476–491. conference: end_date: 2011-08-05 location: Wrocław, Poland name: 'CADE 23: Automated Deduction ' start_date: 2011-07-31 date_created: 2018-12-11T12:02:40Z date_published: 2011-07-19T00:00:00Z date_updated: 2023-02-23T12:23:48Z day: '19' department: - _id: ToHe doi: 10.1007/978-3-642-22438-6_36 intvolume: ' 6803' language: - iso: eng month: '07' oa_version: None page: 476 - 491 publication_status: published publisher: Springer publist_id: '3312' quality_controlled: '1' related_material: record: - id: '5383' relation: earlier_version status: public scopus_import: 1 status: public title: An efficient decision procedure for imperative tree data structures type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 6803 year: '2011' ...