---
_id: '4476'
abstract:
- lang: eng
  text: 'One approach to model checking software is based on the abstract-check-refine
    paradigm: build an abstract model, then check the desired property, and if the
    check fails, refine the model and start over. We introduce the concept of lazy
    abstraction to integrate and optimize the three phases of the abstract-check-refine
    loop. Lazy abstraction continuously builds and refines a single abstract model
    on demand, driven by the model checker, so that different parts of the model may
    exhibit different degrees of precision, namely just enough to verify the desired
    property. We present an algorithm for model checking safety properties using lazy
    abstraction and describe an implementation of the algorithm applied to C programs.
    We also provide sufficient conditions for the termination of the method.'
acknowledgement: "We thank Wes Weimer and Jeff Foster for many useful discussions.
  \r\n"
article_processing_charge: No
author:
- 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: Ranjit
  full_name: Jhala, Ranjit
  last_name: Jhala
- first_name: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
- first_name: Grégoire
  full_name: Sutre, Grégoire
  last_name: Sutre
citation:
  ama: 'Henzinger TA, Jhala R, Majumdar R, Sutre G. Lazy abstraction. In: <i>Proceedings
    of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages</i>.
    ACM; 2002:58-70. doi:<a href="https://doi.org/10.1145/503272.503279">10.1145/503272.503279</a>'
  apa: 'Henzinger, T. A., Jhala, R., Majumdar, R., &#38; Sutre, G. (2002). Lazy abstraction.
    In <i>Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming
    languages</i> (pp. 58–70). Portland, OR, USA: ACM. <a href="https://doi.org/10.1145/503272.503279">https://doi.org/10.1145/503272.503279</a>'
  chicago: Henzinger, Thomas A, Ranjit Jhala, Ritankar Majumdar, and Grégoire Sutre.
    “Lazy Abstraction.” In <i>Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium
    on Principles of Programming Languages</i>, 58–70. ACM, 2002. <a href="https://doi.org/10.1145/503272.503279">https://doi.org/10.1145/503272.503279</a>.
  ieee: T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, “Lazy abstraction,”
    in <i>Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming
    languages</i>, Portland, OR, USA, 2002, pp. 58–70.
  ista: 'Henzinger TA, Jhala R, Majumdar R, Sutre G. 2002. Lazy abstraction. Proceedings
    of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages.
    POPL: Principles of Programming Languages, 58–70.'
  mla: Henzinger, Thomas A., et al. “Lazy Abstraction.” <i>Proceedings of the 29th
    ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages</i>, ACM,
    2002, pp. 58–70, doi:<a href="https://doi.org/10.1145/503272.503279">10.1145/503272.503279</a>.
  short: T.A. Henzinger, R. Jhala, R. Majumdar, G. Sutre, in:, Proceedings of the
    29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM,
    2002, pp. 58–70.
conference:
  end_date: 2002-01-18
  location: Portland, OR, USA
  name: 'POPL: Principles of Programming Languages'
  start_date: 2002-01-16
date_created: 2018-12-11T12:09:03Z
date_published: 2002-01-01T00:00:00Z
date_updated: 2023-06-05T07:45:53Z
day: '01'
doi: 10.1145/503272.503279
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 58 - 70
publication: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of
  programming languages
publication_identifier:
  isbn:
  - '9781581134506'
publication_status: published
publisher: ACM
publist_id: '254'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Lazy abstraction
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2002'
...