{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T02:29:20Z","timestamp":1761964160217,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540654933"},{"type":"electronic","value":"9783540492139"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49213-5_4","type":"book-chapter","created":{"date-parts":[[2007,12,9]],"date-time":"2007-12-09T12:03:39Z","timestamp":1197201819000},"page":"81-102","source":"Crossref","is-referenced-by-count":50,"title":["Compositional Reasoning in Model Checking"],"prefix":"10.1007","author":[{"given":"Sergey","family":"Berezin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S\u00e9rgio","family":"Campos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edmund M.","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,5,21]]},"reference":[{"key":"4_CR1","unstructured":"Henrik R. Andersen. Partial model checking (extended abstract). Technical Report ID-TR: 1994-148, Department of Computer Science, Technical University of Denmark, October 1994. Accepted for LICS\u201995."},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Henrik R. Andersen, Colin Stirling, and Glynn Winskel. A compositional proof system for the modal \u03bc-calculus. In Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, pages 144\u2013153, Paris, France, 4\u20137 July 1994. IEEE Computer Society Press. Also as BRICS Report RS-94-34.","DOI":"10.1109\/LICS.1994.316076"},{"key":"4_CR3","unstructured":"S. Berezin, E. Clarke, S. Jha, and W. Marrero. Model checking algorithms for the mu-calculus. Technical Report TR CMU-CS-96-180, Carnegie Mellon University, September 1996."},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"M. C. Browne, E. M. Clarke, and O. Grumberg. Characterizing finite kripke structures in prepositional temporal logic. Theoretical Computer Science, 59(1-2), July 1988.","DOI":"10.1016\/0304-3975(88)90098-9"},{"issue":"8","key":"4_CR5","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677\u2013691, August 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"4_CR6","unstructured":"J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic model checking with partitioned transition relations. In VLSI 91, Edinburgh, Scotland, 1990."},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Jerry R. Burch, Edmund M. Clarke, David E. Long, Kenneth L. McMillan, and David L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits, 13(4):401\u2013424, April 1994.","DOI":"10.1109\/43.275352"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"S. Campos, E. Clarke, W. Marrero, and M. Minea. Veras: a tool for quantitative analysis of finite-state real-time systems. In Workshop on Languages, Compilers and Tools for Real-Time Systems, 1995.","DOI":"10.1109\/REAL.1994.342709"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"S. Campos, E. Clarke, W. Marrero, M. Minea, and H. Hiraishi. Computing quantitative characteristics of finite-state real-time systems. In IEEE Real-Time Systems Symposium, 1994.","DOI":"10.1109\/REAL.1994.342709"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"S. Campos, E. Clarke, and M. Minea. Verifying the performance of the PCI local bus using symbolic techniques. In Proceedings of the IEEE International Conference on Computer Design, pages 73\u201379, 1995.","DOI":"10.1109\/ICCD.1995.528793"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"S. V. Campos. A Quantitative Approach to the Formal Verification of Real-Time System. PhD thesis, SCS, Carnegie Mellon University, 1996.","DOI":"10.1007\/3-540-63166-6_46"},{"key":"4_CR12","unstructured":"E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. E. Long, K. L. McMillan, and L. A. Ness. Verification of the Futurebus+ cache coherence protocol. In L. Claesen, editor, Proceedings of the Eleventh International Symposium on Computer Hardware Description Languages and their Applications. North-Holland, April 1993."},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, D. E. Long, and K. L. McMillan. Compositional model checking. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science, pages 353\u2013362. IEEE Computer Society Press, June 1989.","DOI":"10.1109\/LICS.1989.39190"},{"key":"4_CR14","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the 1989 International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France","author":"O. Coudert","year":"1989","unstructured":"O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines based on symbolic execution. In J. Sifakis, editor, Proceedings of the 1989 International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, volume 407 of Lecture Notes in Computer Science. Springer-Verlag, June 1989."},{"key":"4_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1007\/3-540-60218-6_2","volume-title":"Proceedings of CONCUR\u201995","author":"M. Dam","year":"1995","unstructured":"M. Dam. Compositional proof systems for model checking infinite state processes. In Proceedings of CONCUR\u201995, volume 962 of Lecture Notes in Computer Science, pages 12\u201326. Springer-Verlag, 1995."},{"key":"4_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1007\/BFb0032063","volume-title":"Proceedings 17th ICALP","author":"J.F. Groote","year":"1990","unstructured":"J.F. Groote and F.W. Vaandrager. An efficient algorithm for branching bisimulation and stuttering equivalence. In M. Paterson, editor, Proceedings 17 th ICALP, Warwick, volume 443 of Lecture Notes in Computer Science, pages 626\u2013638. Springer-Verlag, July 1990."},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Orna Grumberg and David Long. Model checking and modular verification. A CM Transactions on Programming Languages and Systems, 16(3):843\u2013871, May 1994.","DOI":"10.1145\/177492.177725"},{"key":"4_CR18","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of the 7th Conference on Concurrency Theory (CONCUR\u201997)","author":"T. A. Henzinger","year":"1997","unstructured":"T. A. Henzinger, O. Kupferman, and S. K. Rajamani. Fair simulation. In Proc. of the 7th Conference on Concurrency Theory (CONCUR\u201997), volume 1243 of LNCS, Warsaw, July 1997."},{"key":"4_CR19","unstructured":"IEEE Computer Society. IEEE Standard for Futurebus +\u2014Logical Protocol Specification, 1994. IEEE Standard 896.1, 1994 Edition."},{"key":"4_CR20","unstructured":"Intel Corporation. PCI Local Bus Specification, 1993."},{"key":"4_CR21","series-title":"Lect Notes Comput Sci","first-page":"386","volume-title":"Proceedings of the REX Workshop on Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness","author":"B. Josko","year":"1989","unstructured":"B. Josko. Verifying the correctness of AADL-modules using model checking. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Proceedings of the REX Workshop on Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, volume 430 of Lecture Notes in Computer Science, pages 386\u2013400. Springer-Verlag, May 1989."},{"key":"4_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1007\/3-540-63166-6_7","volume-title":"Proc. of the 9th conference on Computer-Aided Verification (CAV\u201997)","author":"O. Kupferman","year":"1997","unstructured":"O. Kupferman and M. Y. Vardi. Module checking revisited. In O. Grumberg, editor, Proc. of the 9th conference on Computer-Aided Verification (CAV\u201997), volume 1254 of LNCS, pages 36\u201347, Haifa, June 1997."},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"J. Misra and K. M. Chandy. Proofs of networks of processes. IEEE Transactions on Software Engineering, SE-7(4), July 1981.","DOI":"10.1109\/TSE.1981.230844"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"R. Paige and R. Tarjan. Three efficient algorithms based on partition refinement. SIAM lournal on Computing, 16(6), Dec 1987.","DOI":"10.1137\/0216062"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"A. Pnueli. In transition for global to modular temporal reasoning about programs. In K. R. Apt, editor, Logics and Models of Concurrent Systems, volume 13 of NATO ASI series. Series F, Computer and system sciences. Springer-Verlag, 1984.","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"4_CR26","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1016\/0304-3975(87)90012-0","volume":"49","author":"C. Stirling","year":"1987","unstructured":"C. Stirling. Modal logics for communicating systems. Theoretical Computer Science, 49:311\u2013348, July 1987.","journal-title":"Theoretical Computer Science"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"H. J. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli. Implicit state enumeration of finite state machines using bdd\u2019s. In IEEE Int. Conf. Computer-Aided Design, pages 130\u2013133, 1990.","DOI":"10.1109\/ICCAD.1990.129860"}],"container-title":["Lecture Notes in Computer Science","Compositionality: The Significant Difference"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49213-5_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T13:14:31Z","timestamp":1737638071000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49213-5_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540654933","9783540492139"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-49213-5_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}