{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:16:12Z","timestamp":1725574572541},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540203636"},{"type":"electronic","value":"9783540397243"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39724-3_13","type":"book-chapter","created":{"date-parts":[[2011,1,8]],"date-time":"2011-01-08T02:15:55Z","timestamp":1294452955000},"page":"141-149","source":"Crossref","is-referenced-by-count":3,"title":["An Optimized Symbolic Bounded Model Checking Engine"],"prefix":"10.1007","author":[{"given":"Rachel","family":"Tzoref","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Matusevich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eli","family":"Berger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ilan","family":"Beer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","unstructured":"CUDD-2.3.1, http:\/\/vlsi.Colorado.edu\/fabio"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Beer, I., Ben-David, S., Eisner, C., Landver, A.: RuleBase: An industry-oriented formal verification tool. In: Design Automation Conference, June 1996, pp. 655\u2013660 (1996)","DOI":"10.1145\/240518.240642"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"480","DOI":"10.1007\/3-540-63166-6_53","volume-title":"Computer Aided Verification","author":"I. Beer","year":"1997","unstructured":"Beer, I., Ben-David, S., Eisner, C., Geist, D., Gluhovsky, L., Heyman, T., Landver, A., Paanah, P., Rodeh, Y., Ronin, G., Wolfsthal, Y.: Rulebase: Model checking at IBM. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 480\u2013483. Springer, Heidelberg (1997)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/BFb0028744","volume-title":"Computer Aided Verification","author":"I. Beer","year":"1998","unstructured":"Beer, I., Ben-David, S., Landver, A.: On-the-fly model checking of RCTL formulas. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 184\u2013194. Springer, Heidelberg (1998)"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Bentley, B.: Validating the intel pentium 4 microprocessor. In: Design Automation Conference, pp. 244\u2013248 (2001)","DOI":"10.1145\/378239.378473"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Bertacco, V., Olukotun, K.: Efficient state representation for symbolic simulation. In: 39th ACM\/IEEE Design Automation Conference (2002)","DOI":"10.1145\/513945.513946"},{"key":"13_CR7","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., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Bryant, R., Beatty, D., Brace, K., Cho, K., Sheffler, T.: Cosmos: A compiled simulator for mos circuits. In: Proceedings of the Design Automation Conference, pp. 9\u201316 (1987)","DOI":"10.1145\/37888.37890"},{"issue":"2","key":"13_CR9","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1145\/103516.103519","volume":"38","author":"R.E. Bryant","year":"1991","unstructured":"Bryant, R.E.: Amethodology for hardware verification based on logic simulation. Journal of the ACM (JACM)\u00a038(2), 299\u2013328 (1991)","journal-title":"Journal of the ACM (JACM)"},{"key":"13_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Press, Norwell (1993)"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of the 38th Design Automation Conference, DAC 2001 (2001)","DOI":"10.1145\/378239.379017"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Sheeran, M., Singh, S., Stalmarck, G.: Checking safety properties using induction and a sat-solver. In: Formal Methods in Computer Aided Design (2000)","DOI":"10.1007\/3-540-40922-X_8"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Silva, G.P.M., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. on Computers, 506\u2013516 (1999)","DOI":"10.1109\/12.769433"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Tzoref, R., Matusevich, M., Berger, E., Beer, I.: An optimized symbolic bounded model checking engine. Technical Report H-0185, IBM Haifa Research Laboratory (2003)","DOI":"10.1007\/978-3-540-39724-3_13"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39724-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T18:03:18Z","timestamp":1559930598000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39724-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540203636","9783540397243"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39724-3_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}