---
_id: '4488'
abstract:
- lang: eng
  text: Assume-guarantee reasoning has long been advertised as an important method
    for decomposing proof obligations in system verification. Refinement mappings
    (homomorphisms) have long been advertised as an important method for solving the
    language-inclusion problem in practice. When confronted with large verification
    problems, we therefore attempted to make use of both techniques. We soon found
    that rather than offering instant solutions, the success of assume-guarantee reasoning
    depends critically on the construction of suitable abstraction modules, and the
    success of refinement checking depends critically on the construction of suitable
    witness modules. Moreover, as abstractions need to be witnessed, and witnesses
    abstracted, the process must be iterated. We present here the main lessons we
    learned from our experiments, in limn of a systematic and structured discipline
    for the compositional verification of reactive modules. An infrastructure to support
    this discipline, and automate parts of the verification, has been implemented
    in the tool Mocha.
acknowledgement: This work is supported in part by ONR YIP award N00014-95-1-0520,
  by NSF CAREER award CCR-9501708, by NSF grant CCR-9504469, by ARO MURI grant DAAH-04-96-1-0341,
  and by the SRC contract 97-DC-324.041.
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: 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. You assume, we guarantee: Methodology
    and case studies. In: <i>Proceedings of the 10th International Conference on Computer
    Aided Verification</i>. Vol 1427. Springer; 1998:440-451. doi:<a href="https://doi.org/10.1007/BFb0028765">10.1007/BFb0028765</a>'
  apa: 'Henzinger, T. A., Qadeer, S., &#38; Rajamani, S. (1998). You assume, we guarantee:
    Methodology and case studies. In <i>Proceedings of the 10th International Conference
    on Computer Aided Verification</i> (Vol. 1427, pp. 440–451). Vancouver, Canada:
    Springer. <a href="https://doi.org/10.1007/BFb0028765">https://doi.org/10.1007/BFb0028765</a>'
  chicago: 'Henzinger, Thomas A, Shaz Qadeer, and Sriram Rajamani. “You Assume, We
    Guarantee: Methodology and Case Studies.” In <i>Proceedings of the 10th International
    Conference on Computer Aided Verification</i>, 1427:440–51. Springer, 1998. <a
    href="https://doi.org/10.1007/BFb0028765">https://doi.org/10.1007/BFb0028765</a>.'
  ieee: 'T. A. Henzinger, S. Qadeer, and S. Rajamani, “You assume, we guarantee: Methodology
    and case studies,” in <i>Proceedings of the 10th International Conference on Computer
    Aided Verification</i>, Vancouver, Canada, 1998, vol. 1427, pp. 440–451.'
  ista: 'Henzinger TA, Qadeer S, Rajamani S. 1998. You assume, we guarantee: Methodology
    and case studies. Proceedings of the 10th International Conference on Computer
    Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 1427, 440–451.'
  mla: 'Henzinger, Thomas A., et al. “You Assume, We Guarantee: Methodology and Case
    Studies.” <i>Proceedings of the 10th International Conference on Computer Aided
    Verification</i>, vol. 1427, Springer, 1998, pp. 440–51, doi:<a href="https://doi.org/10.1007/BFb0028765">10.1007/BFb0028765</a>.'
  short: T.A. Henzinger, S. Qadeer, S. Rajamani, in:, Proceedings of the 10th International
    Conference on Computer Aided Verification, Springer, 1998, pp. 440–451.
conference:
  end_date: 1998-07-02
  location: Vancouver, Canada
  name: 'CAV: Computer Aided Verification'
  start_date: 1998-06-28
date_created: 2018-12-11T12:09:06Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-09-05T07:31:52Z
day: '01'
doi: 10.1007/BFb0028765
extern: '1'
intvolume: '      1427'
language:
- iso: eng
month: '01'
oa_version: None
page: 440 - 451
publication: Proceedings of the 10th International Conference on Computer Aided Verification
publication_identifier:
  isbn:
  - '9783540646082'
publication_status: published
publisher: Springer
publist_id: '239'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'You assume, we guarantee: Methodology and case studies'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1427
year: '1998'
...