{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T13:19:36Z","timestamp":1758633576947,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008989"},{"type":"electronic","value":"9783540365778"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_12","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:04Z","timestamp":1269897124000},"page":"160-175","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["Proof-Like Counter-Examples"],"prefix":"10.1007","author":[{"given":"Arie","family":"Gurfinkel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marsha","family":"Chechik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"12_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"NuSMV: a new Symbolic Model Verifier","author":"A. Cimatti","year":"1999","unstructured":"A. Cimatti, E.M. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: a new Symbolic Model Verifier. In N. Halbwachs and D. Peled, editors, Proceedings of 11th Conference on Computer-Aided Verification (CAV\u201999), number 1633 in Lecture Notes in Computer Science, pages 495\u2013499, Trento, Italy, July 1999. Springer."},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, K.L. McMillan, and X. Zhao. Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. In Proceedings of 32nd Design Automation Conference (DAC 95), pages 427\u2013432, San Francisco, CA, USA, 1995.","DOI":"10.1145\/217474.217565"},{"key":"12_CR3","unstructured":"E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999."},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, Y. Lu, S. Jha, and H. Veith. Tree-Like Counterexamples in Model Checking. In Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science (LICS\u201902), pages 19\u201329, Copenhagen, Denmark, July 2002. IEEE Computer Society.","DOI":"10.1109\/LICS.2002.1029814"},{"key":"12_CR5","unstructured":"M. Fr\u00f6hlich and M. Werner. The Graph Visualization System daVinci \u2014 A user interface for applications. Technical Report 5\/94, Department of Computer Science, Bremen University, 1994."},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"A. Gurfinkel, B. Devereux, and M. Chechik. \u201cModel Exploration with Temporal Logic Query Checking\u201d. In Proceedings of SIGSOFT Conference on Foundations of Software Engineering (FSE\u201902), Charleston, South Carolina, November 2002. ACM Press.","DOI":"10.1145\/587072.587073"},{"key":"12_CR7","unstructured":"A. Gurfinkel. Multi-valued symbolic model-checking: Fairness, counter-examples, running time. Master\u2019s thesis, University of Toronto, Department of Computer Science, October 2002."},{"key":"12_CR8","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/0020-0190(95)00053-F","volume":"54","author":"F. Laroussinie","year":"1995","unstructured":"F. Laroussinie. \u201cAbout the Expressive Power of CTL Combinators\u201d. Information Processing Letters, 54:343\u2013345, 1995.","journal-title":"Information Processing Letters"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"12_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Certifying Model Checkers","author":"K. Namjoshi","year":"2001","unstructured":"K. Namjoshi. Certifying Model Checkers. In Proceedings of 13th International Conference on Computer-AidedVerification (CAV\u201901), volume 2102 of LNCS. Springer-Verlag, 2001."},{"key":"12_CR11","series-title":"Technical report","volume-title":"User Guide for the PVS Specification and Verification System (Draft)","author":"S. Owre","year":"1993","unstructured":"S. Owre, N. Shankar, and J. Rushby. \u201cUser Guide for the PVS Specification and Verification System (Draft)\u201d. Technical report, Computer Science Lab, SRI International, Menlo Park, CA, 1993."},{"key":"12_CR12","series-title":"Lect Notes Comput Sci","volume-title":"FST&TCS","author":"D. Peled","year":"2001","unstructured":"D. Peled, A. Pnueli, and L. Zuck. From falsification to verification. In FST&TCS, volume 2245 of LNCS. Springer-Verlag, 2001."},{"key":"12_CR13","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"From model checking to a temporal proof","author":"D. Peled","year":"2001","unstructured":"D. Peled and L. Zuck. From model checking to a temporal proof. In Proceedings of the 8th International SPINWorkshop (SPIN\u20192001), volume 2057 of LNCS, pages 1\u201314, Toronto, Canada, May 2001. Springer."},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"C. Stirling and D. Walker. Local model-checking in the modal mu-calculus. Theoretical Computer Science, 89, 1991.","DOI":"10.1016\/0304-3975(90)90110-4"},{"key":"12_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1007\/3-540-45657-0_37","volume-title":"Evidence-Based Model Checking","author":"L. Tan","year":"2002","unstructured":"L. Tan and R. Cleaveland. Evidence-Based Model Checking. In Proceedings of 14th Conference on Computer-Aided Verification (CAV\u201902), volume 2404 of LNCS, pages 455\u2013470, Copenhagen, Denmark, July 2002. Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36577-X_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T19:11:07Z","timestamp":1739992267000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"28 February 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}