{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,19]],"date-time":"2024-09-19T15:25:31Z","timestamp":1726759531623},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540544302"},{"type":"electronic","value":"9783540383574"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54430-5_93","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T17:48:06Z","timestamp":1330192086000},"page":"250-265","source":"Crossref","is-referenced-by-count":48,"title":["Model checking and modular verification"],"prefix":"10.1007","author":[{"given":"Orna","family":"Grumberg","sequence":"first","affiliation":[]},{"given":"David E.","family":"Long","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1990.","key":"19_CR1"},{"doi-asserted-by":"crossref","unstructured":"E. M. Clarke, I. A. Draghicescu, and R. P. Kurshan. A unified approach for showing language containment and equivalence between various types of \u03c9-automata. In A. Arnold and N. D. Jones, editors, Proceedings of the 15th Colloquium on Trees in Algebra and Programming, volume 407 of Lecture Notes in Computer Science. Springer-Verlag, May 1990.","key":"19_CR2","DOI":"10.1007\/3-540-52590-4_43"},{"issue":"2","key":"19_CR3","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"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. IEEE Computer Society Press, June 1989.","key":"19_CR4","DOI":"10.1109\/LICS.1989.39190"},{"unstructured":"E. M. Clarke, D. E. Long, and K. L. McMillan. A language for compositional specification and verification of finite state hardware controllers. In J. A. Darringer and F. J. Rammig, editors, Proceedings of the Ninth International Symposium on Computer Hardware Description Languages and their Applications. North-Holland, June 1989.","key":"19_CR5"},{"key":"19_CR6","doi-asserted-by":"crossref","first-page":"725","DOI":"10.1007\/BF00264284","volume":"27","author":"R. Cleaveland","year":"1990","unstructured":"R. Cleaveland. Tableau-based model checking in the propositional mu-calculus. Acta Informatica, 27:725\u2013747, 1990.","journal-title":"Acta Informatica"},{"unstructured":"O. Coudert, C. Berthet, and J. C. Madre. Verifying temporal properties of sequential machines without building their state diagrams. In Kurshan and Clarke [16].","key":"19_CR7"},{"doi-asserted-by":"crossref","unstructured":"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. Springer-Verlag, May 1989.","key":"19_CR8","DOI":"10.1007\/3-540-52559-9"},{"doi-asserted-by":"crossref","unstructured":"D. L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. ACM Distinguished Dissertations, MIT Press, 1989.","key":"19_CR9","DOI":"10.7551\/mitpress\/6874.001.0001"},{"key":"19_CR10","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E. A. Emerson","year":"1986","unstructured":"E. A. Emerson and J. Y. Halpern. \u201cSometimes\u201d and \u201cNot Never\u201d revisited: On branching time versus linear time. Journal of the ACM, 33:151\u2013178, 1986.","journal-title":"Journal of the ACM"},{"unstructured":"E. A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mucalculus. In Proceedings of the Second Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1986.","key":"19_CR11"},{"unstructured":"S. Graf and B. Steffen. Compositional minimization of finite state processes. In Kurshan and Clarke [16].","key":"19_CR12"},{"unstructured":"J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.","key":"19_CR13"},{"unstructured":"B. Josko. Verifying the correctness of AADL-modules using model checking. In de Bakker et al. [8].","key":"19_CR14"},{"unstructured":"R. P. Kurshan. Analysis of discrete event coordination. In de Bakker et al. [8].","key":"19_CR15"},{"unstructured":"R. P. Kurshan and E. M. Clarke, editors. Proceedings of the 1990 Workshop on Computer-Aided Verification, June 1990.","key":"19_CR16"},{"doi-asserted-by":"crossref","unstructured":"R. P. Kurshan and K. L. McMillan. A structural induction theorem for processes. In Proceedings of the Eighth Annual ACM Symposium on Principles of Distributed Computing. ACM Press, August 1989.","key":"19_CR17","DOI":"10.1145\/72981.72998"},{"doi-asserted-by":"crossref","unstructured":"K. G. Larsen. The expressive power of implicit specifications. To appear in Proceedings of the Eighteenth International Colloquium on Automata, Languages, and Programming.","key":"19_CR18","DOI":"10.1007\/3-540-54233-7_135"},{"doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, January 1985.","key":"19_CR19","DOI":"10.1145\/318593.318622"},{"doi-asserted-by":"crossref","unstructured":"R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.","key":"19_CR20","DOI":"10.1007\/3-540-10235-3"},{"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.","key":"19_CR21","DOI":"10.1007\/978-3-642-82453-1_5"},{"doi-asserted-by":"crossref","unstructured":"Z. Shtadler and O. Grumberg. Network grammars, communication behaviors and automatic verification. 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":"19_CR22","DOI":"10.1007\/3-540-52148-8_13"},{"unstructured":"G. Shurek and O. Grumberg. The modular framework of computer-aided verification: Motivation, solutions and evaluation criteria. In Kurshan and Clarke [16].","key":"19_CR23"},{"doi-asserted-by":"crossref","unstructured":"C. Stirling and D. J. Walker. Local model checking in the modal mu-calculus. In J. Diaz and F. Orejas, editors, Proceedings of the 1989 International Joint Conference on Theory and Practice of Software Development, volume 351\u2013352 of Lecture Notes in Computer Science. Springer-Verlag, March 1989.","key":"19_CR24","DOI":"10.1007\/3-540-50939-9_144"},{"doi-asserted-by":"crossref","unstructured":"D. Walker. Bisimulations and divergence. In Proceedings of the Third Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1988.","key":"19_CR25","DOI":"10.1109\/LICS.1988.5117"},{"unstructured":"G. Winskel. Compositional checking of validity on finite state processes. Draft copy.","key":"19_CR26"}],"container-title":["Lecture Notes in Computer Science","CONCUR '91"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54430-5_93.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:54:26Z","timestamp":1605628466000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54430-5_93"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540544302","9783540383574"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-54430-5_93","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}