---
res:
  bibo_abstract:
  - Depth-Bounded Systems form an expressive class of well-structured transition systems.
    They can model a wide range of concurrent infinite-state systems including those
    with dynamic thread creation, dynamically changing communication topology, and
    complex shared heap structures. We present the first method to automatically prove
    fair termination of depth-bounded systems. Our method uses a numerical abstraction
    of the system, which we obtain by systematically augmenting an over-approximation
    of the system’s reachable states with a finite set of counters. This numerical
    abstraction can be analyzed with existing termination provers. What makes our
    approach unique is the way in which it exploits the well-structuredness of the
    analyzed system. We have implemented our work in a prototype tool and used it
    to automatically prove liveness properties of complex concurrent systems, including
    nonblocking algorithms such as Treiber’s stack and several distributed processes.
    Many of these examples are beyond the scope of termination analyses that are based
    on traditional counter abstractions.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Kshitij
      foaf_name: Bansal, Kshitij
      foaf_surname: Bansal
  - foaf_Person:
      foaf_givenName: Eric
      foaf_name: Koskinen, Eric
      foaf_surname: Koskinen
  - 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: Damien
      foaf_name: Zufferey, Damien
      foaf_surname: Zufferey
      foaf_workInfoHomepage: http://www.librecat.org/personId=4397AC76-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-3197-8736
  bibo_doi: 10.1007/978-3-642-36742-7_5
  bibo_volume: 7795
  dct_date: 2013^xs_gYear
  dct_language: eng
  dct_publisher: Springer@
  dct_title: Structural Counter Abstraction@
...