---
res:
  bibo_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.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Thomas
      foaf_name: Wies, Thomas
      foaf_surname: Wies
      foaf_workInfoHomepage: http://www.librecat.org/personId=447BFB88-F248-11E8-B48F-1D18A9856A87
  - foaf_Person:
      foaf_givenName: Marco
      foaf_name: Muñiz, Marco
      foaf_surname: Muñiz
  - foaf_Person:
      foaf_givenName: Viktor
      foaf_name: Kuncak, Viktor
      foaf_surname: Kuncak
  bibo_doi: 10.15479/AT:IST-2011-0005
  dct_date: 2011^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/2664-1690
  dct_language: eng
  dct_publisher: IST Austria@
  dct_title: On an efficient decision procedure for imperative tree data structures@
...