---
res:
  bibo_abstract:
  - 'Modular techniques for automatic verification attempt to overcome the state-explosion
    problem by exploiting the modular structure naturally present in many system designs.
    Unlike other tasks in the verification of finite-state systems, current modular
    techniques rely heavily on user guidance. In particular, the user is typically
    required to construct module abstractions that are neither too detailed as to
    render insufficient benefits in state exploration, nor too coarse as to invalidate
    the desired systemproperties. In this paper, we construct abstractmodules automatically,
    using reachability and controllability information about the concrete modules.
    This allows us to leverage automatic verification techniques by applying them
    in layers: first we compute on the state spaces of system components, then we
    use the results for constructing abstractions, and finally we compute on the abstract
    state space of the system. Our experimental results indicate that if reachability
    and controllability information is used in the construction of abstractions, the
    resulting abstract modules are often significantly smaller than the concrete modules
    and can drastically reduce the space and time requirements for verification.@eng'
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Rajeev
      foaf_name: Alur, Rajeev
      foaf_surname: Alur
  - foaf_Person:
      foaf_givenName: Luca
      foaf_name: De Alfaro, Luca
      foaf_surname: De Alfaro
  - foaf_Person:
      foaf_givenName: Thomas A
      foaf_name: Henzinger, Thomas A
      foaf_surname: Henzinger
      foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
    orcid: 0000−0002−2985−7724
  - foaf_Person:
      foaf_givenName: Freddy
      foaf_name: Mang, Freddy
      foaf_surname: Mang
  bibo_doi: 10.1007/3-540-48320-9_8
  bibo_volume: 1664
  dct_date: 1999^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/9783540664253
  dct_language: eng
  dct_publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik@
  dct_title: Automating modular verification@
...
