---
res:
  bibo_abstract:
  - "Any formal method or tool is almost certainly more often applied in situations
    where the outcome is failure (a counterexample) rather than success (a correctness
    proof). We present a method for symbolic model checking that can lead to significant
    time and memory savings for model-checking runs that fail, while occurring only
    a small overhead for model-checking runs that succeed. Our method discovers an
    error as soon as it cannot be prevented, which can be long before it actually
    occurs; for example, the violation of an invariant may become unpreventable many
    transitions before the invariant is violated.\r\nThe key observation is that “unpreventability”
    is a local property of a single module: an error is unpreventable in a module
    state if no environment can prevent it. Therefore, unpreventability is inexpensive
    to compute for each module, yet can save much work in the state exploration of
    the global, compound system. Based on different degrees of information available
    about the environment, we define and implement several notions of “unpreventability,”
    including the standard notion of uncontrollability from discrete-event control.
    We present experimental results for two examples, a distributed database protocol
    and a wireless communication protocol.@eng"
  bibo_authorlist:
  - 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/10722167_17
  bibo_volume: 1855
  dct_date: 2000^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/9783540677703
  dct_language: eng
  dct_publisher: Springer@
  dct_title: Detecting errors before reaching them@
...