{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:55:16Z","timestamp":1725551716297},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540237389"},{"type":"electronic","value":"9783540304944"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30494-4_13","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T14:42:14Z","timestamp":1277822534000},"page":"174-185","source":"Crossref","is-referenced-by-count":4,"title":["Simple Yet Efficient Improvements of SAT Based Bounded Model Checking"],"prefix":"10.1007","author":[{"given":"Emmanuel","family":"Zarpas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","unstructured":"Accelera. PSL\/Sugar LRM.: \n                  \n                    http:\/\/www.eda.org\/vfv\/"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Beer, I., et al.: RuleBase: An Industry Oriented Formal Verification Tool. In: 33rd Design Automation Conference, DAC 1996. ACM\/IEEE (1996)","DOI":"10.1109\/DAC.1996.545656"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-44585-4_33","volume-title":"Computer Aided Verification","author":"I. Beer","year":"2001","unstructured":"Beer, I., et al.: The Temporal Logic Sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 363. Springer, Heidelberg (2001)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., et al.: Symbolic Model Checking Without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, p. 193. Springer, Heidelberg (1999)"},{"key":"13_CR5","volume-title":"Advances in Computers","author":"A. Biere","year":"2003","unstructured":"Biere, A., et al.: Bounded Model Checking. In: Advances in Computers, vol.\u00a058. Academic Press, London (2003) (pre-print)"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Cook, S.: The Complexity of Theorem Proving Procedures. In: Proceeding, Third Annual ACM Symp. on the Theory of Computing (1971)","DOI":"10.1145\/800157.805047"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. In: Journal of the ACM, vol.\u00a05(7) (1962)","DOI":"10.1145\/368273.368557"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. Een","year":"2004","unstructured":"Een, N., Sorensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"13_CR9","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E. Emerson","year":"1986","unstructured":"Emerson, E., Lei, C.: Modalities for Model Checking: Branching Time Strikes Back. Science of Computer Programming\u00a08, 275\u2013306 (1986)","journal-title":"Science of Computer Programming"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: a Fast and Robust SAT-solver. In: Proceedings of the Design, Automation and Test in Europe. DATE 2002 (2002)","DOI":"10.1109\/DATE.2002.998262"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1007\/978-3-540-24605-3_35","volume-title":"Theory and Applications of Satisfiability Testing","author":"D. Berre Le","year":"2004","unstructured":"Le Berre, D., Simon, L.: The essentials of the SAT 2003 competition. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 468\u2013487. Springer, Heidelberg (2004)"},{"key":"13_CR12","first-page":"530","volume-title":"38th Design Automation Conference","author":"M. Moskewicz","year":"2001","unstructured":"Moskewicz, M., et al.: Chaff: Engineering an Efficient SAT Solver. In: 38th Design Automation Conference, pp. 530\u2013535. ACM\/IEEE, NewYork (2001)"},{"key":"13_CR13","unstructured":"Nadel, A.: JeruSAT satisfiablility solver. Available on-line., \n                  \n                    http:\/\/www.geocities.com\/alikn78\/"},{"key":"13_CR14","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"Pnueli, A.: A Temporal Logic of Concurrent Programs. Theoretical Computer Science\u00a013, 45\u201360 (1981)","journal-title":"Theoretical Computer Science"},{"key":"13_CR15","volume-title":"Proceeding of the 4th International Workshop on Microprocessor, Test and Verification","author":"O. Shacham","year":"2003","unstructured":"Shacham, O., Zarpas, E.: Tuning the VSIDS Decision Heuristic for Bounded Model Checking. In: Proceeding of the 4th International Workshop on Microprocessor, Test and Verification. IEEE Computer Society, Austin (2003)"},{"key":"13_CR16","unstructured":"Silva, J., Sakallah, K.: Grasp - a New Search Algorithm for Satisfiability. In: Technical Report TR-CSE-292996, University of Michigan (1996)"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"O. Strichman","year":"2000","unstructured":"Strichman, O.: Tuning SAT Checkers for Bounded Model Checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/3-540-49519-3_18","volume-title":"Formal Methods in Computer-Aided Design","author":"B. Yang","year":"1998","unstructured":"Yang, B., et al.: A Performance Study of BDD-Bases Model Checking. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 255\u2013289. Springer, Heidelberg (1998)"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/3-540-45657-0_2","volume-title":"Computer Aided Verification","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: The Quest for Efficient Boolean Satisfiability Solvers. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 17. Springer, Heidelberg (2002)"},{"key":"13_CR20","unstructured":"Berkley Logic Interechange Format (BLIF). University of California, Berkley (1992), \n                  \n                    http:\/\/www-cad.eecs.berkeley.edu\/Respep\/Research\/vis\/usrDoc.html"},{"key":"13_CR21","unstructured":"IBM Formal Verification Benchmark Library., \n                  \n                    http:\/\/www.haifa.il.ibm.com\/projects\/verification\/RB_Homepage\/fvbenchmarks.html"},{"key":"13_CR22","unstructured":"Benchmarks, C.N.F.: from IBM Formal Verification Benchmarks Library., \n                  \n                    http:\/\/www.haifa.il.ibm.com\/projects\/verification\/RB_Homepage\/bmcbenchmarks.html"},{"key":"13_CR23","unstructured":"IBM CNF Benchmark Illustration., \n                  \n                    http:\/\/www.haifa.il.ibm.com\/projects\/verification\/RB_Homepage\/bmcbenchmarks_illustrations.html"},{"key":"13_CR24","unstructured":"Web version of the RuleBase User Manual., \n                  \n                    http:\/\/www.haifa.il.ibm.com\/projects\/verification\/RB_Homepage\/"},{"key":"13_CR25","unstructured":"RuleBase University Program, \n                  \n                    http:\/\/www.haifa.il.ibm.com\/projects\/verification\/Formal_Methods-Home\/university.html"},{"key":"13_CR26","unstructured":"SAT2004 contest., \n                  \n                    http:\/\/satlive.org\/SATCompetition\/2004\/"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30494-4_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T00:04:33Z","timestamp":1620000273000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30494-4_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540237389","9783540304944"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30494-4_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}