---
_id: '4638'
abstract:
- lang: eng
  text: "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."
acknowledgement: This research was supported in part by the DARPA (NASA) grant NAG2-1214,
  the SRC contract 99-TJ-683.003, the MARCO grant 98-DT-660, the DARPA (MARCO) grant
  MDA972-99-1-0001, and the NSF CAREER award CCR-9501708.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Luca
  full_name: De Alfaro, Luca
  last_name: De Alfaro
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Freddy
  full_name: Mang, Freddy
  last_name: Mang
citation:
  ama: 'De Alfaro L, Henzinger TA, Mang F. Detecting errors before reaching them.
    In: <i>Proceedings of the 12th International Conference on Computer Aided Verification</i>.
    Vol 1855. Springer; 2000:186-201. doi:<a href="https://doi.org/10.1007/10722167_17">10.1007/10722167_17</a>'
  apa: 'De Alfaro, L., Henzinger, T. A., &#38; Mang, F. (2000). Detecting errors before
    reaching them. In <i>Proceedings of the 12th International Conference on Computer
    Aided Verification</i> (Vol. 1855, pp. 186–201). Chicago, IL, USA: Springer. <a
    href="https://doi.org/10.1007/10722167_17">https://doi.org/10.1007/10722167_17</a>'
  chicago: De Alfaro, Luca, Thomas A Henzinger, and Freddy Mang. “Detecting Errors
    before Reaching Them.” In <i>Proceedings of the 12th International Conference
    on Computer Aided Verification</i>, 1855:186–201. Springer, 2000. <a href="https://doi.org/10.1007/10722167_17">https://doi.org/10.1007/10722167_17</a>.
  ieee: L. De Alfaro, T. A. Henzinger, and F. Mang, “Detecting errors before reaching
    them,” in <i>Proceedings of the 12th International Conference on Computer Aided
    Verification</i>, Chicago, IL, USA, 2000, vol. 1855, pp. 186–201.
  ista: 'De Alfaro L, Henzinger TA, Mang F. 2000. Detecting errors before reaching
    them. Proceedings of the 12th International Conference on Computer Aided Verification.
    CAV: Computer-Aided Verification, LNCS, vol. 1855, 186–201.'
  mla: De Alfaro, Luca, et al. “Detecting Errors before Reaching Them.” <i>Proceedings
    of the 12th International Conference on Computer Aided Verification</i>, vol.
    1855, Springer, 2000, pp. 186–201, doi:<a href="https://doi.org/10.1007/10722167_17">10.1007/10722167_17</a>.
  short: L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of the 12th International
    Conference on Computer Aided Verification, Springer, 2000, pp. 186–201.
conference:
  end_date: 2000-07-19
  location: Chicago, IL, USA
  name: 'CAV: Computer-Aided Verification'
  start_date: 2000-07-15
date_created: 2018-12-11T12:09:53Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-13T13:18:06Z
day: '01'
doi: 10.1007/10722167_17
extern: '1'
intvolume: '      1855'
language:
- iso: eng
month: '01'
oa_version: None
page: 186 - 201
publication: Proceedings of the 12th International Conference on Computer Aided Verification
publication_identifier:
  isbn:
  - '9783540677703'
publication_status: published
publisher: Springer
publist_id: '70'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Detecting errors before reaching them
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1855
year: '2000'
...