---
_id: '4470'
abstract:
- lang: eng
  text: Giotto is a platform-independent language for specifying software for high-performance
    control applications. In this paper we present a new approach to the compilation
    of Giotto. Following this approach, the Giotto compiler generates code for a virtual
    machine, called the E machine, which can be ported to different platforms. The
    Giotto compiler also checks if the generated E code is time safe for a given platform,
    that is, if the platform offers sufficient performance to ensure that the E code
    is executed in a timely fashion that conforms with the Giotto semantics. Time-safety
    checking requires a schedulability analysis. We show that while for arbitrary
    E code, the analysis is exponential, for E code generated from typical Giotto
    programs, the analysis is polynomial. This supports our claim that Giotto identifies
    a useful fragment of embedded programs.
acknowledgement: Supported in part by the DARPA SEC grant F33615-C-98-3614, MARCO
  GSRC grant 98-DT-660, AFOSR MURI grant F49620-00-1-0327, NSF grant CCR-9988172,
  and a Microsoft Research Fellowship.
alternative_title:
- LNCS
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: Christoph
  full_name: Kirsch, Christoph
  last_name: Kirsch
- first_name: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
- first_name: Slobodan
  full_name: Matic, Slobodan
  last_name: Matic
citation:
  ama: 'Henzinger TA, Kirsch C, Majumdar R, Matic S. Time-safety checking for embedded
    programs. In: <i>Proceedings of the 2nd International Conference on Embedded Software</i>.
    Vol 2491. ACM; 2002:76-92. doi:<a href="https://doi.org/10.1007/3-540-45828-X_7">10.1007/3-540-45828-X_7</a>'
  apa: 'Henzinger, T. A., Kirsch, C., Majumdar, R., &#38; Matic, S. (2002). Time-safety
    checking for embedded programs. In <i>Proceedings of the 2nd International Conference
    on Embedded Software</i> (Vol. 2491, pp. 76–92). Grenoble, France: ACM. <a href="https://doi.org/10.1007/3-540-45828-X_7">https://doi.org/10.1007/3-540-45828-X_7</a>'
  chicago: Henzinger, Thomas A, Christoph Kirsch, Ritankar Majumdar, and Slobodan
    Matic. “Time-Safety Checking for Embedded Programs.” In <i>Proceedings of the
    2nd International Conference on Embedded Software</i>, 2491:76–92. ACM, 2002.
    <a href="https://doi.org/10.1007/3-540-45828-X_7">https://doi.org/10.1007/3-540-45828-X_7</a>.
  ieee: T. A. Henzinger, C. Kirsch, R. Majumdar, and S. Matic, “Time-safety checking
    for embedded programs,” in <i>Proceedings of the 2nd International Conference
    on Embedded Software</i>, Grenoble, France, 2002, vol. 2491, pp. 76–92.
  ista: 'Henzinger TA, Kirsch C, Majumdar R, Matic S. 2002. Time-safety checking for
    embedded programs. Proceedings of the 2nd International Conference on Embedded
    Software. EMSOFT: Embedded Software , LNCS, vol. 2491, 76–92.'
  mla: Henzinger, Thomas A., et al. “Time-Safety Checking for Embedded Programs.”
    <i>Proceedings of the 2nd International Conference on Embedded Software</i>, vol.
    2491, ACM, 2002, pp. 76–92, doi:<a href="https://doi.org/10.1007/3-540-45828-X_7">10.1007/3-540-45828-X_7</a>.
  short: T.A. Henzinger, C. Kirsch, R. Majumdar, S. Matic, in:, Proceedings of the
    2nd International Conference on Embedded Software, ACM, 2002, pp. 76–92.
conference:
  end_date: 2002-10-09
  location: Grenoble, France
  name: 'EMSOFT: Embedded Software '
  start_date: 2002-10-07
date_created: 2018-12-11T12:09:01Z
date_published: 2002-09-25T00:00:00Z
date_updated: 2023-06-05T08:50:59Z
day: '25'
doi: 10.1007/3-540-45828-X_7
extern: '1'
intvolume: '      2491'
language:
- iso: eng
month: '09'
oa_version: None
page: 76 - 92
publication: Proceedings of the 2nd International Conference on Embedded Software
publication_identifier:
  isbn:
  - '9783540443070'
publication_status: published
publisher: ACM
publist_id: '259'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Time-safety checking for embedded programs
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2491
year: '2002'
...
---
_id: '4471'
abstract:
- lang: eng
  text: The sequential synthesis problem, which is closely related to Church’s solvability
    problem, asks, given a specification in the form of a binary relation between
    input and output streams, for the construction of a finite-state stream transducer
    that converts inputs to appropriate outputs. For efficiency reasons, practical
    sequential hardware is often designed to operate without prior initialization.
    Such hardware designs can be modeled by uninitialized state machines, which are
    required to satisfy their specification if started from any state. In this paper
    we solve the sequential synthesis problem for uninitialized systems, that is,
    we construct uninitialized finite-state stream transducers. We consider specifications
    given by LTL formulas, deterministic, nondeterministic, universal, and alternating
    Büchi automata. We solve this uninitialized synthesis problem by reducing it to
    the well-understood initialized synthesis problem. While our solution is straightforward,
    it leads, for some specification formalisms, to upper bounds that are exponentially
    worse than the complexity of the corresponding initialized problems. However,
    we prove lower bounds to show that our simple solutions are optimal for all considered
    specification formalisms. We also study the problem of deciding whether a given
    specification is uninitialized, that is, if its uninitialized and initialized
    synthesis problems coincide. We show that this problem has, for each specification
    formalism, the same complexity as the equivalence problem.
acknowledgement: This research was supported in part by the SRC contract 99-TJ-683.003,
  the DARPA contract NAG2-1214, and the NSF grant CCR-9988172.
alternative_title:
- LNCS
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: Sriram
  full_name: Krishnan, Sriram
  last_name: Krishnan
- first_name: Orna
  full_name: Kupferman, Orna
  last_name: Kupferman
- first_name: Freddy
  full_name: Mang, Freddy
  last_name: Mang
citation:
  ama: 'Henzinger TA, Krishnan S, Kupferman O, Mang F. Synthesis of uninitialized
    systems. In: <i>Proceedings of the 29th International Colloquium on Automata,
    Languages and Programming</i>. Vol 2380. Springer; 2002:644-656. doi:<a href="https://doi.org/10.1007/3-540-45465-9_55">10.1007/3-540-45465-9_55</a>'
  apa: 'Henzinger, T. A., Krishnan, S., Kupferman, O., &#38; Mang, F. (2002). Synthesis
    of uninitialized systems. In <i>Proceedings of the 29th International Colloquium
    on Automata, Languages and Programming</i> (Vol. 2380, pp. 644–656). Malaga, Spain:
    Springer. <a href="https://doi.org/10.1007/3-540-45465-9_55">https://doi.org/10.1007/3-540-45465-9_55</a>'
  chicago: Henzinger, Thomas A, Sriram Krishnan, Orna Kupferman, and Freddy Mang.
    “Synthesis of Uninitialized Systems.” In <i>Proceedings of the 29th International
    Colloquium on Automata, Languages and Programming</i>, 2380:644–56. Springer,
    2002. <a href="https://doi.org/10.1007/3-540-45465-9_55">https://doi.org/10.1007/3-540-45465-9_55</a>.
  ieee: T. A. Henzinger, S. Krishnan, O. Kupferman, and F. Mang, “Synthesis of uninitialized
    systems,” in <i>Proceedings of the 29th International Colloquium on Automata,
    Languages and Programming</i>, Malaga, Spain, 2002, vol. 2380, pp. 644–656.
  ista: 'Henzinger TA, Krishnan S, Kupferman O, Mang F. 2002. Synthesis of uninitialized
    systems. Proceedings of the 29th International Colloquium on Automata, Languages
    and Programming. ICALP: Automata, Languages and Programming, LNCS, vol. 2380,
    644–656.'
  mla: Henzinger, Thomas A., et al. “Synthesis of Uninitialized Systems.” <i>Proceedings
    of the 29th International Colloquium on Automata, Languages and Programming</i>,
    vol. 2380, Springer, 2002, pp. 644–56, doi:<a href="https://doi.org/10.1007/3-540-45465-9_55">10.1007/3-540-45465-9_55</a>.
  short: T.A. Henzinger, S. Krishnan, O. Kupferman, F. Mang, in:, Proceedings of the
    29th International Colloquium on Automata, Languages and Programming, Springer,
    2002, pp. 644–656.
conference:
  end_date: 2002-07-13
  location: Malaga, Spain
  name: 'ICALP: Automata, Languages and Programming'
  start_date: 2002-07-08
date_created: 2018-12-11T12:09:01Z
date_published: 2002-06-26T00:00:00Z
date_updated: 2023-06-05T08:05:13Z
day: '26'
doi: 10.1007/3-540-45465-9_55
extern: '1'
intvolume: '      2380'
language:
- iso: eng
month: '06'
oa_version: None
page: 644 - 656
publication: Proceedings of the 29th International Colloquium on Automata, Languages
  and Programming
publication_identifier:
  isbn:
  - '9783540438649'
publication_status: published
publisher: Springer
publist_id: '257'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Synthesis of uninitialized systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2380
year: '2002'
...
---
_id: '4472'
abstract:
- lang: eng
  text: 'We present a methodology and tool for verifying and certifying systems code.
    The verification is based on the lazy-abstraction paradigm for intertwining the
    following three logical steps: construct a predicate abstraction from the code,
    model check the abstraction, and automatically refine the abstraction based on
    counterexample analysis. The certification is based on the proof-carrying code
    paradigm. Lazy abstraction enables the automatic construction of small proof certificates.
    The methodology is implemented in Blast, the Berkeley Lazy Abstraction Software
    verification Tool. We describe our experience applying Blast to Linux and Windows
    device drivers. Given the C code for a driver and for a temporal-safety monitor,
    Blast automatically generates an easily checkable correctness certificate if the
    driver satisfies the specification, and an error trace otherwise.'
acknowledgement: This work was supported in part by the NSF ITR grants CCR-0085949,
  CCR-0081588, the NSF Career grant CCR-9875171, the DARPA PCES grant F33615-00-C-1693,
  the MARCO GSRC grant 98-DT-660, the SRC contract 99-TJ-683, a Microsoft fellowship,
  and gifts from AT&T Research and Microsoft Research.
alternative_title:
- LNCS
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: George
  full_name: Necula, George
  last_name: Necula
- first_name: Ranjit
  full_name: Jhala, Ranjit
  last_name: Jhala
- first_name: Grégoire
  full_name: Sutre, Grégoire
  last_name: Sutre
- first_name: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
- first_name: Westley
  full_name: Weimer, Westley
  last_name: Weimer
citation:
  ama: 'Henzinger TA, Necula G, Jhala R, Sutre G, Majumdar R, Weimer W. Temporal safety
    proofs for systems code. In: <i>Proceedings of the 14th International Conference
    on Computer Aided Verification</i>. Vol 2404. Springer; 2002:526-538. doi:<a href="https://doi.org/10.1007/3-540-45657-0_45">10.1007/3-540-45657-0_45</a>'
  apa: 'Henzinger, T. A., Necula, G., Jhala, R., Sutre, G., Majumdar, R., &#38; Weimer,
    W. (2002). Temporal safety proofs for systems code. In <i>Proceedings of the 14th
    International Conference on Computer Aided Verification</i> (Vol. 2404, pp. 526–538).
    Copenhagen, Denmark: Springer. <a href="https://doi.org/10.1007/3-540-45657-0_45">https://doi.org/10.1007/3-540-45657-0_45</a>'
  chicago: Henzinger, Thomas A, George Necula, Ranjit Jhala, Grégoire Sutre, Ritankar
    Majumdar, and Westley Weimer. “Temporal Safety Proofs for Systems Code.” In <i>Proceedings
    of the 14th International Conference on Computer Aided Verification</i>, 2404:526–38.
    Springer, 2002. <a href="https://doi.org/10.1007/3-540-45657-0_45">https://doi.org/10.1007/3-540-45657-0_45</a>.
  ieee: T. A. Henzinger, G. Necula, R. Jhala, G. Sutre, R. Majumdar, and W. Weimer,
    “Temporal safety proofs for systems code,” in <i>Proceedings of the 14th International
    Conference on Computer Aided Verification</i>, Copenhagen, Denmark, 2002, vol.
    2404, pp. 526–538.
  ista: 'Henzinger TA, Necula G, Jhala R, Sutre G, Majumdar R, Weimer W. 2002. Temporal
    safety proofs for systems code. Proceedings of the 14th International Conference
    on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 2404,
    526–538.'
  mla: Henzinger, Thomas A., et al. “Temporal Safety Proofs for Systems Code.” <i>Proceedings
    of the 14th International Conference on Computer Aided Verification</i>, vol.
    2404, Springer, 2002, pp. 526–38, doi:<a href="https://doi.org/10.1007/3-540-45657-0_45">10.1007/3-540-45657-0_45</a>.
  short: T.A. Henzinger, G. Necula, R. Jhala, G. Sutre, R. Majumdar, W. Weimer, in:,
    Proceedings of the 14th International Conference on Computer Aided Verification,
    Springer, 2002, pp. 526–538.
conference:
  end_date: 2002-07-31
  location: Copenhagen, Denmark
  name: 'CAV: Computer Aided Verification'
  start_date: 2002-07-27
date_created: 2018-12-11T12:09:01Z
date_published: 2002-06-19T00:00:00Z
date_updated: 2023-06-05T08:11:32Z
day: '19'
doi: 10.1007/3-540-45657-0_45
extern: '1'
intvolume: '      2404'
language:
- iso: eng
month: '06'
oa_version: None
page: 526 - 538
publication: Proceedings of the 14th International Conference on Computer Aided Verification
publication_identifier:
  isbn:
  - '9783540439974'
publication_status: published
publisher: Springer
publist_id: '258'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Temporal safety proofs for systems code
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2404
year: '2002'
...
---
_id: '4473'
abstract:
- lang: eng
  text: 'The simulation preorder on state transition systems is widely accepted as
    a useful notion of refinement, both in its own right and as an efficiently checkable
    sufficient condition for trace containment. For composite systems, due to the
    exponential explosion of the state space, there is a need for decomposing a simulation
    check of the form P ≤s Q, denoting &quot;P is simulated by Q,&quot; into simpler
    simulation checks on the components of P and Q. We present an assume-guarantee
    rule that enables such a decomposition. To the best of our knowledge, this is
    the first assume-guarantee rule that applies to a refinement relation different
    from trace containment. Our rule is circular, and its soundness proof requires
    induction on trace trees. The proof is constructive: given simulation relations
    that witness the simulation preorder between corresponding components of P and
    Q, we provide a procedure for constructing a witness relation for P ≤s Q. We also
    extend our assume-guarantee rule to account for fairness constraints on transition
    systems.'
article_processing_charge: No
article_type: original
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: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
- first_name: Sriram
  full_name: Rajamani, Sriram
  last_name: Rajamani
- first_name: Serdar
  full_name: Tasiran, Serdar
  last_name: Tasiran
citation:
  ama: Henzinger TA, Qadeer S, Rajamani S, Tasiran S. An assume-guarantee rule for
    checking simulation. <i>ACM Transactions on Programming Languages and Systems
    (TOPLAS)</i>. 2002;24(1):51-64. doi:<a href="https://doi.org/10.1145/509705.509707">10.1145/509705.509707</a>
  apa: Henzinger, T. A., Qadeer, S., Rajamani, S., &#38; Tasiran, S. (2002). An assume-guarantee
    rule for checking simulation. <i>ACM Transactions on Programming Languages and
    Systems (TOPLAS)</i>. ACM. <a href="https://doi.org/10.1145/509705.509707">https://doi.org/10.1145/509705.509707</a>
  chicago: Henzinger, Thomas A, Shaz Qadeer, Sriram Rajamani, and Serdar Tasiran.
    “An Assume-Guarantee Rule for Checking Simulation.” <i>ACM Transactions on Programming
    Languages and Systems (TOPLAS)</i>. ACM, 2002. <a href="https://doi.org/10.1145/509705.509707">https://doi.org/10.1145/509705.509707</a>.
  ieee: T. A. Henzinger, S. Qadeer, S. Rajamani, and S. Tasiran, “An assume-guarantee
    rule for checking simulation,” <i>ACM Transactions on Programming Languages and
    Systems (TOPLAS)</i>, vol. 24, no. 1. ACM, pp. 51–64, 2002.
  ista: Henzinger TA, Qadeer S, Rajamani S, Tasiran S. 2002. An assume-guarantee rule
    for checking simulation. ACM Transactions on Programming Languages and Systems
    (TOPLAS). 24(1), 51–64.
  mla: Henzinger, Thomas A., et al. “An Assume-Guarantee Rule for Checking Simulation.”
    <i>ACM Transactions on Programming Languages and Systems (TOPLAS)</i>, vol. 24,
    no. 1, ACM, 2002, pp. 51–64, doi:<a href="https://doi.org/10.1145/509705.509707">10.1145/509705.509707</a>.
  short: T.A. Henzinger, S. Qadeer, S. Rajamani, S. Tasiran, ACM Transactions on Programming
    Languages and Systems (TOPLAS) 24 (2002) 51–64.
date_created: 2018-12-11T12:09:02Z
date_published: 2002-01-01T00:00:00Z
date_updated: 2023-06-05T07:59:47Z
day: '01'
doi: 10.1145/509705.509707
extern: '1'
intvolume: '        24'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 51 - 64
publication: ACM Transactions on Programming Languages and Systems (TOPLAS)
publication_identifier:
  issn:
  - 0164-0925
publication_status: published
publisher: ACM
publist_id: '256'
quality_controlled: '1'
scopus_import: '1'
status: public
title: An assume-guarantee rule for checking simulation
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 24
year: '2002'
...
---
_id: '4474'
abstract:
- lang: eng
  text: 'The simulation preorder for labeled transition systems is defined locally,
    and operationally, as a game that relates states with their immediate successor
    states. Simulation enjoys many appealing properties. First, simulation has a denotational
    characterization: system S simulates system I iff every computation tree embedded
    in the unrolling of I can be embedded also in the unrolling of S. Second, simulation
    has a logical characterization: S simulates I iff every universal branching-time
    formula satisfied by S is satisfied also by I. It follows that simulation is a
    suitable notion of implementation, and it is the coarsest abstraction of a system
    that preserves universal branching-time properties. Third, based on its local
    definition, simulation between finite-state systems can be checked in polynomial
    time. Finally, simulation implies trace containment, which cannot be defined locally
    and requires polynomial space for verification. Hence simulation is widely used
    both in manual and in automatic verification. Liveness assumptions about transition
    systems are typically modeled using fairness constraints. Existing notions of
    simulation for fair transition systems, however, are not local, and as a result,
    many appealing properties of the simulation preorder are lost. We propose a new
    view of fair simulation by extending the local definition of simulation to account
    for fairness: system View the MathML sourcefairly simulates system View the MathML
    source iff in the simulation game, there is a strategy that matches with each
    fair computation of View the MathML source a fair computation of View the MathML
    source. Our definition enjoys a denotational characterization and has a logical
    characterization: View the MathML source fairly simulates View the MathML source
    iff every fair computation tree (whose infinite paths are fair) embedded in the
    unrolling of View the MathML source can be embedded also in the unrolling of View
    the MathML source or, equivalently, iff every Fair-∀AFMC formula satisfied by
    View the MathML source is satisfied also by View the MathML source (∀AFMC is the
    universal fragment of the alternation-free μ-calculus). The locality of the definition
    leads us to a polynomial-time algorithm for checking fair simulation for finite-state
    systems with weak and strong fairness constraints. Finally, fair simulation implies
    fair trace containment and is therefore useful as an efficiently computable local
    criterion for proving linear-time abstraction hierarchies of fair systems.'
acknowledgement: We thank Ramin Hojati, Doron Bustan, and the anonymous reviewers
  for their comments on this paper.
article_processing_charge: No
article_type: original
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: Orna
  full_name: Kupferman, Orna
  last_name: Kupferman
- first_name: Sriram
  full_name: Rajamani, Sriram
  last_name: Rajamani
citation:
  ama: Henzinger TA, Kupferman O, Rajamani S. Fair simulation. <i>Information and
    Computation</i>. 2002;173(1):64-81. doi:<a href="https://doi.org/10.1006/inco.2001.3085">10.1006/inco.2001.3085</a>
  apa: Henzinger, T. A., Kupferman, O., &#38; Rajamani, S. (2002). Fair simulation.
    <i>Information and Computation</i>. Elsevier. <a href="https://doi.org/10.1006/inco.2001.3085">https://doi.org/10.1006/inco.2001.3085</a>
  chicago: Henzinger, Thomas A, Orna Kupferman, and Sriram Rajamani. “Fair Simulation.”
    <i>Information and Computation</i>. Elsevier, 2002. <a href="https://doi.org/10.1006/inco.2001.3085">https://doi.org/10.1006/inco.2001.3085</a>.
  ieee: T. A. Henzinger, O. Kupferman, and S. Rajamani, “Fair simulation,” <i>Information
    and Computation</i>, vol. 173, no. 1. Elsevier, pp. 64–81, 2002.
  ista: Henzinger TA, Kupferman O, Rajamani S. 2002. Fair simulation. Information
    and Computation. 173(1), 64–81.
  mla: Henzinger, Thomas A., et al. “Fair Simulation.” <i>Information and Computation</i>,
    vol. 173, no. 1, Elsevier, 2002, pp. 64–81, doi:<a href="https://doi.org/10.1006/inco.2001.3085">10.1006/inco.2001.3085</a>.
  short: T.A. Henzinger, O. Kupferman, S. Rajamani, Information and Computation 173
    (2002) 64–81.
date_created: 2018-12-11T12:09:02Z
date_published: 2002-02-25T00:00:00Z
date_updated: 2023-06-05T07:53:27Z
day: '25'
doi: 10.1006/inco.2001.3085
extern: '1'
intvolume: '       173'
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://www.sciencedirect.com/science/article/pii/S0890540101930858?via%3Dihub
month: '02'
oa: 1
oa_version: Published Version
page: 64 - 81
publication: Information and Computation
publication_identifier:
  issn:
  - 0890-5401
publication_status: published
publisher: Elsevier
publist_id: '255'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Fair simulation
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 173
year: '2002'
...
---
_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'
...