{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T13:41:14Z","timestamp":1737034874345,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439974"},{"type":"electronic","value":"9783540456575"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45657-0_21","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T14:59:43Z","timestamp":1179586783000},"page":"280-294","source":"Crossref","is-referenced-by-count":3,"title":["Semi-formal Bounded Model Checking"],"prefix":"10.1007","author":[{"given":"Jesse D.","family":"Bingham","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan J.","family":"Hu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,20]]},"reference":[{"key":"21_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for Construction and Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic model checking without BDDs. In Tools and Algorithms for Construction and Analysis of Systems, pages 193\u2013207. LNCS 1579. Springer, 1999."},{"key":"21_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"418","DOI":"10.1007\/3-540-48683-6_36","volume-title":"Computer-Aided Verification: Eleventh International Conference","author":"V. Boppana","year":"1999","unstructured":"Vamsi Boppana, Sreeranga P. Rajan, Koichiro Takayama, and Masahiro Fujita. Model checking based on sequential ATPG. In Computer-Aided Verification: Eleventh International Conference, pages 418\u2013430. LNCS 1633. Springer, 1999."},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In Conference on Logic in Computer Science, pages 428\u2013439, 1990.","DOI":"10.1109\/LICS.1990.113767"},{"key":"21_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Workshop on Logics of Programs","author":"E. M. Clarke","year":"1982","unstructured":"Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Dexter Kozen, editor, Workshop on Logics of Programs, pages 52\u201371, May 1981. Published as LNCS 131. Springer, 1982."},{"issue":"7","key":"21_CR5","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"Martin Davis","year":"1962","unstructured":"Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem proving. Communications of the ACM, 5(7):394\u2013397, July 1962.","journal-title":"Communications of the ACM"},{"issue":"3","key":"21_CR6","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"Martin Davis","year":"1960","unstructured":"Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201\u2013215, July 1960.","journal-title":"Journal of the ACM"},{"key":"21_CR7","unstructured":"David Goldberg. Computer Arithmetic. Appendix A in D. A. Patterson and J. L. Hennessy, Computer Architecture: A Quantitative Approach, 2nd Ed., Morgan Kaufmann, 1996."},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Jo\u00e3o P. Marques Silva and Karem A. Sakallah. GRASP \u2014 a new search algorithm for satisfiability. In International Conference on Computer-Aided Design, pages 220\u2013227. IEEE\/ACM, 1996.","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In 38th Design Automation Conference, pages 530\u2013535. ACM\/IEEE, 2001.","DOI":"10.1145\/378239.379017"},{"key":"21_CR10","series-title":"Lect Notes Comput Sci","first-page":"337","volume-title":"5th International Symposium on Programming","author":"J.-P. Queille","year":"1981","unstructured":"Jean-Pierre Queille and Joseph Sifakis. Specification and verification of concurrent systems in Cesar. In 5th International Symposium on Programming, pages 337\u2013351. LNCS 137. Springer, 1981."},{"key":"21_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/10722167_36","volume-title":"Computer-Aided Verification: 12th International Conference","author":"O. Shtrichman","year":"2000","unstructured":"Ofer Shtrichman. Tuning SAT checkers for bounded model checking. In Computer-Aided Verification: 12th International Conference, pages 480\u2013494. LNCS 1855. Springer, 2000."},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Hantao Zhang. SATO: An efficient propositional prover. In 14th Conference on Automated Deduction, pages 272\u2013275. LNAI 1249. Springer, 1997.","DOI":"10.1007\/3-540-63104-6_28"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45657-0_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T13:10:57Z","timestamp":1737033057000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45657-0_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439974","9783540456575"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-45657-0_21","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}