{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:16:51Z","timestamp":1725488211638},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540644064"},{"type":"electronic","value":"9783540697787"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-69778-0_3","type":"book-chapter","created":{"date-parts":[[2007,8,4]],"date-time":"2007-08-04T09:02:30Z","timestamp":1186218150000},"page":"18-24","source":"Crossref","is-referenced-by-count":2,"title":["Model Checking: Historical Perspective and Example (Extended Abstract)"],"prefix":"10.1007","author":[{"given":"Edmund M.","family":"Clarke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergey","family":"Berezin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2000,7,21]]},"reference":[{"key":"3_CR1","unstructured":"S. Bose and A. L. Fisher. Automatic verification of synchronous circuits using symbolic logic simulation and temporal logic. In L. Claesen, editor, Proceedings of the IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, November 1989."},{"key":"3_CR2","unstructured":"M. C. Browne and E. M. Clarke. Sml: A high level language for the design and verification of finite state machines. In IFIP WG 10.2 International Working Conference from HDL Descriptions to Guaranteed Correct Circuit Designs, Grenoble, France. IFIP, September 1986."},{"key":"3_CR3","unstructured":"M. C. Browne, E. M. Clarke, and D. Dill. Checking the correctness of sequential circuits. In Proceedings of the 1985 International Conference on Computer Design, Port Chester, New York, October 1985. IEEE."},{"key":"3_CR4","unstructured":"M. C. Browne, E. M. Clarke, and D. Dill. Automatic circuit verification using temporal logic: Two new examples. In Formal Aspects of VLSI Design. Elsevier Science Publishers (North Holland), 1986."},{"issue":"12","key":"3_CR5","doi-asserted-by":"publisher","first-page":"1035","DOI":"10.1109\/TC.1986.1676711","volume":"C-35","author":"M. C. Browne","year":"1986","unstructured":"M. C. Browne, E. M. Clarke, D. L. Dill, and B. Mishra. Automatic verification of sequential circuits using temporal logic. IEEE Transactions on Computers, C-35(12):1035\u20131044, December 1986.","journal-title":"IEEE Transactions on Computers"},{"issue":"8","key":"3_CR6","doi-asserted-by":"publisher","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":"3_CR7","unstructured":"J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic model checking with partitioned transition relations. In A. Halaas and P. B. Denyer, editors, Proceedings of the 1991 International Conference on Very Large Scale Integration, August 1991. Winner of the Sidney Michaelson Best Paper Award."},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Sequential circuit verification using symbolic model checking. In Proceedings of the 27th ACM\/IEEE Design Automation Conference, pages 46\u201351. IEEE Computer Society Press, June 1990.","DOI":"10.1145\/123186.123223"},{"issue":"2","key":"3_CR9","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. R. Burch","year":"1992","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, June 1992.","journal-title":"Information and Computation"},{"key":"3_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Logic of Programs: Workshop, Yorktown Heights, NY, May 1981","author":"E. M. Clarke","year":"1981","unstructured":"E. M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In D. Kozen, editor, Logic of Programs: Workshop, Yorktown Heights, NY, May 1981, volume 131 of Lecture Notes in Computer Science. Springer-Verlag, 1981."},{"issue":"2","key":"3_CR11","doi-asserted-by":"publisher","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, April 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"3_CR12","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":"3_CR13","doi-asserted-by":"crossref","unstructured":"O. Coudert, J. C. Madre, and C. Berthet. Verifying temporal properties of sequential machines without building their state diagrams. In E. M. Clarke, editors. Proceedings of the 1990 Workshop on computer-Aided Verification. Springer-Verlag, June 1990 Kurshan and Clarke [19].","DOI":"10.1090\/dimacs\/003\/07"},{"key":"3_CR14","series-title":"Technical Report NASA Contractor Report","volume-title":"Finite-state analysis of space shuttle contingency guidance requirements","author":"J. Crow","year":"1996","unstructured":"Judith Crow. Finite-state analysis of space shuttle contingency guidance requirements. Technical Report NASA Contractor Report 4741, SRI International, Menlo Park, CA, May 1996."},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"D. L. Dill and E. M. Clarke. Automatic verification of asynchronous circuits using temporal logic. IEE Proceedings, Part E 133(5), 1986.","DOI":"10.1049\/ip-e.1986.0034"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and Chin Laung Lei. Modalities for model checking: Branching time strikes back. Twelfth Symposium on Principles of Programming Languages, New Orleans, La., January 1985.","DOI":"10.1145\/318593.318620"},{"issue":"1","key":"3_CR17","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1002\/j.1538-7305.1990.tb00102.x","volume":"69","author":"Z. Har\u2019El","year":"1990","unstructured":"Z. Har\u2019El and R. P. Kurshan. Software for analytical development of communications protocols. AT&T Technical Journal, 69(1):45\u201359, Jan.\u2013Feb. 1990.","journal-title":"AT&T Technical Journal"},{"key":"3_CR18","series-title":"Lect Notes Comput Sci","first-page":"414","volume-title":"Proceedings of the REX Workshop on Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness","author":"R. P. Kurshan","year":"1989","unstructured":"R. P. Kurshan. Analysis of discrete event coordination. 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 414\u2013453. Springer-Verlag, May 1989."},{"key":"3_CR19","unstructured":"R. P. Kurshan and E. M. Clarke, editors. Proceedings of the 1990 Workshop on Computer-Aided Verification. Springer-Verlag, June 1990."},{"key":"3_CR20","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, pages 97\u2013107. Association for Computing Machinery, January 1985.","DOI":"10.1145\/318593.318622"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. PhD thesis, Carnegie Mellon University, 1992.","DOI":"10.1007\/978-1-4615-3190-6_3"},{"key":"3_CR22","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0304-3975(85)90223-3","volume":"38","author":"B. Mishra","year":"1985","unstructured":"B. Mishra and E.M. Clarke. Hierarchical verification of asynchronous circuits using temporal logic. Theoretical Computer Science, 38:269\u2013291, 1985.","journal-title":"Theoretical Computer Science"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"C. Pixley. A computational theory and implementation of sequential hardware equivalence. In R. Kurshan and E. Clarke, editors, Proc. CAV Workshop (also DIMACS Tech. Report 90-31), Rutgers University, NJ, June 1990.","DOI":"10.1090\/dimacs\/003\/20"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"C. Pixley, G. Beihl, and E. Pacas-Skewes. Automatic derivation of FSM specification to implementation encoding. In Proceedings of the International Conference on Computer Desgin, pages 245\u2013249, Cambridge, MA, October 1991.","DOI":"10.1109\/ICCD.1991.139891"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"C. Pixley, S.-W. Jeong, and G. D. Hachtel. Exact calculation of synchronization sequences based on binary decision diagrams. In Proceedings of the 29th Design Automation Conference, pages 620\u2013623, June 1992.","DOI":"10.1109\/DAC.1992.227811"},{"key":"3_CR26","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"A. Pnueli. A temporal logic of concurrent programs. Theoretical Computer Science, 13:45\u201360, 1981.","journal-title":"Theoretical Computer Science"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"J. P. Quielle and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proceedings of the Fifth International Symposium in Programming, 1982.","DOI":"10.1007\/3-540-11494-7_22"},{"issue":"3","key":"3_CR28","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A. P. Sistla","year":"1986","unstructured":"A. P. Sistla and E.M. Clarke. Complexity of propositional temporal logics. Journal of the ACM, 32(3):733\u2013749, July 1986.","journal-title":"Journal of the ACM"},{"key":"3_CR29","unstructured":"M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1986."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-69778-0_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,25]],"date-time":"2020-04-25T16:32:28Z","timestamp":1587832348000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-69778-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540644064","9783540697787"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-69778-0_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}