{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T08:10:13Z","timestamp":1737360613246,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540421245"},{"type":"electronic","value":"9783540451396"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45139-0_1","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T14:39:56Z","timestamp":1186756796000},"page":"1-14","source":"Crossref","is-referenced-by-count":21,"title":["From model checking to a temporal proof"],"prefix":"10.1007","author":[{"given":"Doron","family":"Peled","sequence":"first","affiliation":[]},{"given":"Lenore","family":"Zuck","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,5,2]]},"reference":[{"key":"1_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Workshop on Logic of Programs","author":"E. M. Clarke","year":"1981","unstructured":"E. M. Clarke, E. A. Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic. Workshop on Logic of Programs, Yorktown Heights, NY, 1981, LNCS 131, Springer-Verlag."},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"G. Bhat, R. Cleaveland, O. Grumberg, Efficient on-the-fly model checking for CTL*. Logic in Computer Science, 1995, San Diego, CA, 388\u2013397","DOI":"10.1109\/LICS.1995.523273"},{"key":"1_CR3","unstructured":"E. M. Clarke, O. Grumberg, D. Peled, Model Checking, MIT Press, 2000."},{"key":"1_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/3-540-10003-2_69","volume-title":"Automata, Languages and Programming","author":"E. A. Emerson","year":"1980","unstructured":"E. A. Emerson, E. M. Clarke, Characterizing correctness properties of parallel programs using fixpoints, LNCS 85, Springer Verlag, Automata, Languages and Programming, July 1980, 169\u2013181."},{"key":"1_CR5","first-page":"3","volume-title":"Protocol Specification Testing and Verification","author":"R. Gerth","year":"1995","unstructured":"R. Gerth, D. Peled, M. Y. Vardi,, P. Wolper, Simple on-the-fly automatic verification of linear temporal logic, Protocol Specification Testing and Verification, 3\u201318, Warsaw, Poland, 1995. Chapman & Hall."},{"key":"1_CR6","unstructured":"G. J. Holzmann, Design and Validation of Computer Protocols, Prentice-Hall Software Series, 1992."},{"key":"1_CR7","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"R.P. Kurshan","year":"1994","unstructured":"R.P. Kurshan. Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton, New Jersey,1994."},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer, 1991.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"K. Namjoshi, Certifying model checkers, Submitted to CAV 2001.","DOI":"10.1007\/3-540-44585-4_2"},{"key":"1_CR10","unstructured":"M. Y. Vardi, P. Wolper, An automata-theoretic approach to automatic program verification. Proc. 1st Annual Symposium on Logic in Computer Science IEEE, 1986."}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45139-0_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T07:35:40Z","timestamp":1737358540000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45139-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540421245","9783540451396"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-45139-0_1","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}