{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T04:19:37Z","timestamp":1768277977380,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540374060","type":"print"},{"value":"9783540374114","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11817963_18","type":"book-chapter","created":{"date-parts":[[2006,8,5]],"date-time":"2006-08-05T01:07:51Z","timestamp":1154740071000},"page":"170-174","source":"Crossref","is-referenced-by-count":39,"title":["Yasm: A Software Model-Checker for Verification and Refutation"],"prefix":"10.1007","author":[{"given":"Arie","family":"Gurfinkel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ou","family":"Wei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marsha","family":"Chechik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"18_CR1","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/s10009-002-0095-0","volume":"5","author":"T. Ball","year":"2003","unstructured":"Ball, T., Podelski, A., Rajamani, S.: Boolean and Cartesian Abstraction for Model Checking C Programs. STTT\u00a05(1), 49\u201358 (2003)","journal-title":"STTT"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2004","unstructured":"Barrett, C., Berezin, S.: CVC Lite: A New Implementation of the Cooperating Validity Checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"issue":"4","key":"18_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/990010.990011","volume":"12","author":"M. Chechik","year":"2003","unstructured":"Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: Multi-Valued Symbolic Model-Checking. ACM TOSEM\u00a012(4), 1\u201338 (2003)","journal-title":"ACM TOSEM"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/3-540-45657-0_41","volume-title":"Computer Aided Verification","author":"M. Chechik","year":"2002","unstructured":"Chechik, M., Devereux, B., Gurfinkel, A.: \u03c7Chek: A Multi-Valued Model-Checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 505\u2013509. Springer, Heidelberg (2002)"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-540-31984-9_17","volume-title":"Fundamental Approaches to Software Engineering","author":"M. Chechik","year":"2005","unstructured":"Chechik, M., Gurfinkel, A.: A Framework for Counterexample Generation and Exploration. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol.\u00a03442, pp. 217\u2013233. Springer, Heidelberg (2005)"},{"issue":"5","key":"18_CR6","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E. Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement for Symbolic Model Checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"issue":"19","key":"18_CR7","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"2","author":"D. Dams","year":"1997","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Abstract Interpretation of Reactive Systems. ACM TOPLAS\u00a02(19), 253\u2013291 (1997)","journal-title":"ACM TOPLAS"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Dams, D., Namjoshi, K.S.: The Existence of Finite Abstractions for Branching Time Model Checking. In: LICS 2004, pp. 335\u2013344 (2004)","DOI":"10.1109\/LICS.2004.1319628"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/3-540-44685-0_29","volume-title":"CONCUR 2001 - Concurrency Theory","author":"P. Godefroid","year":"2001","unstructured":"Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based Model Checking using Modal Transition Systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 426\u2013440. Springer, Heidelberg (2001)"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-36577-X_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Gurfinkel","year":"2003","unstructured":"Gurfinkel, A., Chechik, M.: Proof-Like Counter-Examples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 160\u2013175. Springer, Heidelberg (2003)"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/11691372_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Gurfinkel","year":"2006","unstructured":"Gurfinkel, A., Chechik, M.: Why Waste a Perfectly Good Abstraction? In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 212\u2013226. Springer, Heidelberg (2006)"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: POPL 2002, pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"G. Necula","year":"2002","unstructured":"Necula, G., McPeak, S., Rahul, S., Weimer, W.: CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol.\u00a02304, pp. 213\u2013228. Springer, Heidelberg (2002)"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11513988_7","volume-title":"Computer Aided Verification","author":"C. Pasareanu","year":"2005","unstructured":"Pasareanu, C., Pelanek, R., Visser, W.: Concrete Model Checking with Abstract Matching and Refinement. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 52\u201366. Springer, Heidelberg (2005)"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-540-45069-6_28","volume-title":"Computer Aided Verification","author":"S. Shoham","year":"2003","unstructured":"Shoham, S., Grumberg, O.: A Game-Based Framework for CTL Counter-Examples and 3-Valued Abstraction-Refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 275\u2013287. Springer, Heidelberg (2003)"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/978-3-540-24730-2_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Shoham","year":"2004","unstructured":"Shoham, S., Grumberg, O.: Monotonic Abstraction-Refinement for CTL. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 546\u2013560. Springer, Heidelberg (2004)"},{"key":"18_CR17","unstructured":"Somenzi, F.: CUDD: CU Decision Diagram Package Release (2001)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11817963_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T03:30:00Z","timestamp":1619494200000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11817963_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540374060","9783540374114"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/11817963_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}