[{"status":"public","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_published":"1998-01-01T00:00:00Z","type":"conference","publist_id":"103","publication_identifier":{"isbn":["9783540646082"]},"language":[{"iso":"eng"}],"conference":{"end_date":"1998-07-02","location":"Vancouver, Canada","name":"CAV: Computer Aided Verification","start_date":"1998-06-28"},"publication":"Proceedings of the 10th International Conference on Computer Aided Verification","month":"01","oa_version":"None","extern":"1","volume":1427,"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.","date_updated":"2022-08-23T09:06:21Z","citation":{"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.","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>.","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>","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."},"year":"1998","doi":"10.1007/BFb0028774","day":"01","page":"521 - 525","quality_controlled":"1","publisher":"Springer","author":[{"first_name":"Rajeev","last_name":"Alur","full_name":"Alur, Rajeev"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Mang","first_name":"Freddy","full_name":"Mang, Freddy"},{"full_name":"Qadeer, Shaz","last_name":"Qadeer","first_name":"Shaz"},{"full_name":"Rajamani, Sriram","first_name":"Sriram","last_name":"Rajamani"},{"full_name":"Tasiran, Serdar","first_name":"Serdar","last_name":"Tasiran"}],"_id":"4604","scopus_import":"1","alternative_title":["LNCS"],"title":"Mocha: Modularity in model checking","intvolume":"      1427","publication_status":"published","date_created":"2018-12-11T12:09:42Z","article_processing_charge":"No"},{"date_updated":"2022-09-05T07:31:52Z","citation":{"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>","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>","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.","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>.","short":"T.A. Henzinger, S. Qadeer, S. Rajamani, in:, Proceedings of the 10th International Conference on Computer Aided Verification, Springer, 1998, pp. 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>.","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."},"year":"1998","doi":"10.1007/BFb0028765","day":"01","abstract":[{"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.","lang":"eng"}],"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.","volume":1427,"extern":"1","_id":"4488","scopus_import":"1","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"full_name":"Qadeer, Shaz","last_name":"Qadeer","first_name":"Shaz"},{"full_name":"Rajamani, Sriram","last_name":"Rajamani","first_name":"Sriram"}],"publication_status":"published","date_created":"2018-12-11T12:09:06Z","article_processing_charge":"No","title":"You assume, we guarantee: Methodology and case studies","alternative_title":["LNCS"],"intvolume":"      1427","page":"440 - 451","quality_controlled":"1","publisher":"Springer","date_published":"1998-01-01T00:00:00Z","type":"conference","publication_identifier":{"isbn":["9783540646082"]},"publist_id":"239","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","status":"public","publication":"Proceedings of the 10th International Conference on Computer Aided Verification","oa_version":"None","month":"01","language":[{"iso":"eng"}],"conference":{"location":"Vancouver, Canada","end_date":"1998-07-02","name":"CAV: Computer Aided Verification","start_date":"1998-06-28"}},{"extern":"1","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.","volume":1427,"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."}],"doi":"10.1007/BFb0028745","day":"01","date_updated":"2022-08-24T09:19:53Z","year":"1998","citation":{"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.","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.","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>.","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>"},"publisher":"Springer","page":"195 - 206","quality_controlled":"1","title":"From pre-historic to post-modern symbolic model checking","alternative_title":["LNCS"],"intvolume":"      1427","publication_status":"published","article_processing_charge":"No","date_created":"2018-12-11T12:09:07Z","author":[{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Kupferman","first_name":"Orna","full_name":"Kupferman, Orna"},{"first_name":"Shaz","last_name":"Qadeer","full_name":"Qadeer, Shaz"}],"_id":"4489","scopus_import":"1","status":"public","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publist_id":"240","publication_identifier":{"isbn":["9783540646082"]},"date_published":"1998-01-01T00:00:00Z","type":"conference","conference":{"end_date":"1998-07-02","location":"Vancouver, Canada","name":"CAV: Computer Aided Verification","start_date":"1998-06-28"},"language":[{"iso":"eng"}],"month":"01","oa_version":"None","publication":"Proceedings of the 10th International Conference on Computer Aided Verification"}]