---
_id: '4604'
acknowledgement: This research was supported in part by the ONR YIP award N00014-95-1-0520,
  by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the 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: Rajeev
  full_name: Alur, Rajeev
  last_name: Alur
- 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: Freddy
  full_name: Mang, Freddy
  last_name: Mang
- 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: 'Alur R, Henzinger TA, Mang F, Qadeer S, Rajamani S, Tasiran S. Mocha: Modularity
    in model checking. In: <i>Proceedings of the 10th International Conference on
    Computer Aided Verification</i>. Vol 1427. Springer; 1998:521-525. doi:<a href="https://doi.org/10.1007/BFb0028774">10.1007/BFb0028774</a>'
  apa: 'Alur, R., Henzinger, T. A., Mang, F., Qadeer, S., Rajamani, S., &#38; Tasiran,
    S. (1998). Mocha: Modularity in model checking. In <i>Proceedings of the 10th
    International Conference on Computer Aided Verification</i> (Vol. 1427, pp. 521–525).
    Vancouver, Canada: Springer. <a href="https://doi.org/10.1007/BFb0028774">https://doi.org/10.1007/BFb0028774</a>'
  chicago: 'Alur, Rajeev, Thomas A Henzinger, Freddy Mang, Shaz Qadeer, Sriram Rajamani,
    and Serdar Tasiran. “Mocha: Modularity in Model Checking.” In <i>Proceedings of
    the 10th International Conference on Computer Aided Verification</i>, 1427:521–25.
    Springer, 1998. <a href="https://doi.org/10.1007/BFb0028774">https://doi.org/10.1007/BFb0028774</a>.'
  ieee: 'R. Alur, T. A. Henzinger, F. Mang, S. Qadeer, S. Rajamani, and S. Tasiran,
    “Mocha: Modularity in model checking,” in <i>Proceedings of the 10th International
    Conference on Computer Aided Verification</i>, Vancouver, Canada, 1998, vol. 1427,
    pp. 521–525.'
  ista: 'Alur R, Henzinger TA, Mang F, Qadeer S, Rajamani S, Tasiran S. 1998. Mocha:
    Modularity in model checking. Proceedings of the 10th International Conference
    on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 1427,
    521–525.'
  mla: 'Alur, Rajeev, et al. “Mocha: Modularity in Model Checking.” <i>Proceedings
    of the 10th International Conference on Computer Aided Verification</i>, vol.
    1427, Springer, 1998, pp. 521–25, doi:<a href="https://doi.org/10.1007/BFb0028774">10.1007/BFb0028774</a>.'
  short: R. Alur, T.A. Henzinger, F. Mang, S. Qadeer, S. Rajamani, S. Tasiran, in:,
    Proceedings of the 10th International Conference on Computer Aided Verification,
    Springer, 1998, pp. 521–525.
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:42Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-23T09:06:21Z
day: '01'
doi: 10.1007/BFb0028774
extern: '1'
intvolume: '      1427'
language:
- iso: eng
month: '01'
oa_version: None
page: 521 - 525
publication: Proceedings of the 10th International Conference on Computer Aided Verification
publication_identifier:
  isbn:
  - '9783540646082'
publication_status: published
publisher: Springer
publist_id: '103'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Mocha: Modularity in model checking'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1427
year: '1998'
...
---
_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'
...
---
_id: '4489'
abstract:
- lang: eng
  text: "Symbolic model checking, which enables the automatic verification of large
    systems, proceeds by calculating with expressions that represent state sets. Traditionally,
    symbolic model-checking tools arc based on backward state traversal; their basic
    operation is the function pre, which given a set of states, returns the set of
    all predecessor states. This is because specifiers usally employ formalisms with
    future-time modalities. which are naturally evaluated by iterating applications
    of pre. It has been recently shown experimentally that symbolic model checking
    can perform significantly better if it is based, instead, on forward state traversal;
    in this case, the basic operation is the function post, which given a set of states,
    returns the set of all successor states. This is because forward state traversal
    can ensure that only those parts of the state space are explored which are reachable
    from an initial state and relevant for satisfaction or violation of the specification;
    that is, errors can be detected as soon as possible.\r\nIn this paper, we investigate
    which specifications can be checked by symbolic forward state traversal. We formulate
    the problems of symbolic backward and forward model checking by means of two -calculi.
    The pre- calculus is based on the pre operation; the post- calculus, on the post
    operation. These two -calculi induce query logics, which augment fixpoint expressions
    with a boolean emptiness query. Using query logics, we are able to relate and
    compare the symbolic backward and forward approaches. In particular, we prove
    that all -regular (linear-time) specifications can be expressed as post- queries,
    and therefore checked using symbolic forward state traversal. On the other hand,
    we show that there are simple branching-time specifications that cannot be checked
    in this way."
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: Orna
  full_name: Kupferman, Orna
  last_name: Kupferman
- first_name: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
citation:
  ama: 'Henzinger TA, Kupferman O, Qadeer S. From pre-historic to post-modern symbolic
    model checking. In: <i>Proceedings of the 10th International Conference on Computer
    Aided Verification</i>. Vol 1427. Springer; 1998:195-206. doi:<a href="https://doi.org/10.1007/BFb0028745">10.1007/BFb0028745</a>'
  apa: 'Henzinger, T. A., Kupferman, O., &#38; Qadeer, S. (1998). From pre-historic
    to post-modern symbolic model checking. In <i>Proceedings of the 10th International
    Conference on Computer Aided Verification</i> (Vol. 1427, pp. 195–206). Vancouver,
    Canada: Springer. <a href="https://doi.org/10.1007/BFb0028745">https://doi.org/10.1007/BFb0028745</a>'
  chicago: Henzinger, Thomas A, Orna Kupferman, and Shaz Qadeer. “From Pre-Historic
    to Post-Modern Symbolic Model Checking.” In <i>Proceedings of the 10th International
    Conference on Computer Aided Verification</i>, 1427:195–206. Springer, 1998. <a
    href="https://doi.org/10.1007/BFb0028745">https://doi.org/10.1007/BFb0028745</a>.
  ieee: T. A. Henzinger, O. Kupferman, and S. Qadeer, “From pre-historic to post-modern
    symbolic model checking,” in <i>Proceedings of the 10th International Conference
    on Computer Aided Verification</i>, Vancouver, Canada, 1998, vol. 1427, pp. 195–206.
  ista: 'Henzinger TA, Kupferman O, Qadeer S. 1998. From pre-historic to post-modern
    symbolic model checking. Proceedings of the 10th International Conference on Computer
    Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 1427, 195–206.'
  mla: Henzinger, Thomas A., et al. “From Pre-Historic to Post-Modern Symbolic Model
    Checking.” <i>Proceedings of the 10th International Conference on Computer Aided
    Verification</i>, vol. 1427, Springer, 1998, pp. 195–206, doi:<a href="https://doi.org/10.1007/BFb0028745">10.1007/BFb0028745</a>.
  short: T.A. Henzinger, O. Kupferman, S. Qadeer, in:, Proceedings of the 10th International
    Conference on Computer Aided Verification, Springer, 1998, pp. 195–206.
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:07Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2022-08-24T09:19:53Z
day: '01'
doi: 10.1007/BFb0028745
extern: '1'
intvolume: '      1427'
language:
- iso: eng
month: '01'
oa_version: None
page: 195 - 206
publication: Proceedings of the 10th International Conference on Computer Aided Verification
publication_identifier:
  isbn:
  - '9783540646082'
publication_status: published
publisher: Springer
publist_id: '240'
quality_controlled: '1'
scopus_import: '1'
status: public
title: From pre-historic to post-modern symbolic model checking
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1427
year: '1998'
...