---
_id: '4483'
abstract:
- lang: eng
  text: 'Model-checking algorithms can be used to verify, formally and automatically,
    if a low-level description of a design conforms with a high-level description.
    However, for designs with very large state spaces, prior to the application of
    an algorithm, the refinement-checking task needs to be decomposed into subtasks
    of manageable complexity. It is natural to decompose the task following the component
    structure of the design. However, an individual component often does not satisfy
    its requirements unless the component is put into the right context, which constrains
    the inputs to the component. Thus, in order to verify each component individually,
    we need to make assumptions about its inputs, which are provided by the other
    components of the design. This reasoning is circular: component A is verified
    under the assumption that context B behaves correctly, and symmetrically, B is
    verified assuming the correctness of A. The assume-guarantee paradigm provides
    a systematic theory and methodology for ensuring the soundness of the circular
    style of postulating and discharging assumptions in component-based reasoning.We
    give a tutorial introduction to the assume-guarantee paradigm for decomposing
    refinement-checking tasks. To illustrate the method, we step in detail through
    the formal verification of a processor pipeline against an instruction set architecture.
    In this example, the verification of a three-stage pipeline is broken up into
    three subtasks, one for each stage of the pipeline.'
acknowledgement: 'Supported in part by DARPA Information Technology Office, by the
  MARC0 Gigascale Silicon Research Center, and by the National Science Foundation. '
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: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
- first_name: Sriram
  full_name: Rajamani, Sriram
  last_name: Rajamani
citation:
  ama: 'Henzinger TA, Qadeer S, Rajamani S. Decomposing refinement proofs using assume-guarantee
    reasoning. In: <i>Proceedings of the 2000 International Conference on Computer-Aided
    Design</i>. IEEE; 2000:245-252. doi:<a href="https://doi.org/10.1109/ICCAD.2000.896481">10.1109/ICCAD.2000.896481</a>'
  apa: 'Henzinger, T. A., Qadeer, S., &#38; Rajamani, S. (2000). Decomposing refinement
    proofs using assume-guarantee reasoning. In <i>Proceedings of the 2000 International
    Conference on Computer-Aided Design</i> (pp. 245–252). San Jose, CA, USA: IEEE.
    <a href="https://doi.org/10.1109/ICCAD.2000.896481">https://doi.org/10.1109/ICCAD.2000.896481</a>'
  chicago: Henzinger, Thomas A, Shaz Qadeer, and Sriram Rajamani. “Decomposing Refinement
    Proofs Using Assume-Guarantee Reasoning.” In <i>Proceedings of the 2000 International
    Conference on Computer-Aided Design</i>, 245–52. IEEE, 2000. <a href="https://doi.org/10.1109/ICCAD.2000.896481">https://doi.org/10.1109/ICCAD.2000.896481</a>.
  ieee: T. A. Henzinger, S. Qadeer, and S. Rajamani, “Decomposing refinement proofs
    using assume-guarantee reasoning,” in <i>Proceedings of the 2000 International
    Conference on Computer-Aided Design</i>, San Jose, CA, USA, 2000, pp. 245–252.
  ista: 'Henzinger TA, Qadeer S, Rajamani S. 2000. Decomposing refinement proofs using
    assume-guarantee reasoning. Proceedings of the 2000 International Conference on
    Computer-Aided Design. ICCAD: Computer-Aided Design, 245–252.'
  mla: Henzinger, Thomas A., et al. “Decomposing Refinement Proofs Using Assume-Guarantee
    Reasoning.” <i>Proceedings of the 2000 International Conference on Computer-Aided
    Design</i>, IEEE, 2000, pp. 245–52, doi:<a href="https://doi.org/10.1109/ICCAD.2000.896481">10.1109/ICCAD.2000.896481</a>.
  short: T.A. Henzinger, S. Qadeer, S. Rajamani, in:, Proceedings of the 2000 International
    Conference on Computer-Aided Design, IEEE, 2000, pp. 245–252.
conference:
  end_date: 2000-11-09
  location: San Jose, CA, USA
  name: 'ICCAD: Computer-Aided Design'
  start_date: 2000-11-05
date_created: 2018-12-11T12:09:05Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2023-04-18T12:57:52Z
day: '01'
doi: 10.1109/ICCAD.2000.896481
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 245 - 252
publication: Proceedings of the 2000 International Conference on Computer-Aided Design
publication_identifier:
  isbn:
  - '0780364457'
publication_status: published
publisher: IEEE
publist_id: '249'
quality_controlled: '1'
status: public
title: Decomposing refinement proofs using assume-guarantee reasoning
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2000'
...