---
_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.'
author:
- first_name: Thomas A
full_name: Thomas Henzinger
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 K
last_name: Rajamani
citation:
ama: 'Henzinger TA, Qadeer S, Rajamani S. Decomposing refinement proofs using assume-guarantee
reasoning. In: IEEE; 2000:245-252. doi:10.1109/ICCAD.2000.896481'
apa: 'Henzinger, T. A., Qadeer, S., & Rajamani, S. (2000). Decomposing refinement
proofs using assume-guarantee reasoning (pp. 245–252). Presented at the ICCAD:
Computer-Aided Design, IEEE. https://doi.org/10.1109/ICCAD.2000.896481'
chicago: Henzinger, Thomas A, Shaz Qadeer, and Sriram Rajamani. “Decomposing Refinement
Proofs Using Assume-Guarantee Reasoning,” 245–52. IEEE, 2000. https://doi.org/10.1109/ICCAD.2000.896481.
ieee: 'T. A. Henzinger, S. Qadeer, and S. Rajamani, “Decomposing refinement proofs
using assume-guarantee reasoning,” presented at the ICCAD: Computer-Aided Design,
2000, pp. 245–252.'
ista: 'Henzinger TA, Qadeer S, Rajamani S. 2000. Decomposing refinement proofs using
assume-guarantee reasoning. ICCAD: Computer-Aided Design, 245–252.'
mla: Henzinger, Thomas A., et al. *Decomposing Refinement Proofs Using Assume-Guarantee
Reasoning*. IEEE, 2000, pp. 245–52, doi:10.1109/ICCAD.2000.896481.
short: T.A. Henzinger, S. Qadeer, S. Rajamani, in:, IEEE, 2000, pp. 245–252.
conference:
name: 'ICCAD: Computer-Aided Design'
date_created: 2018-12-11T12:09:05Z
date_published: 2000-01-01T00:00:00Z
date_updated: 2021-01-12T07:57:17Z
day: '01'
doi: 10.1109/ICCAD.2000.896481
extern: 1
month: '01'
page: 245 - 252
publication_status: published
publisher: IEEE
publist_id: '249'
quality_controlled: 0
status: public
title: Decomposing refinement proofs using assume-guarantee reasoning
type: conference
year: '2000'
...