{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T16:00:42Z","timestamp":1725552042358},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540340218"},{"type":"electronic","value":"9783540340225"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11750321_58","type":"book-chapter","created":{"date-parts":[[2006,5,4]],"date-time":"2006-05-04T06:11:16Z","timestamp":1146723076000},"page":"611-620","source":"Crossref","is-referenced-by-count":1,"title":["Improved SAT Based Bounded Model Checking"],"prefix":"10.1007","author":[{"given":"Conghua","family":"Zhou","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Decheng","family":"Ding","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"58_CR1","volume-title":"Model checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press, Cambridge (2000)"},{"key":"58_CR2","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/BF01257083","volume":"20","author":"M. Ben-Ari","year":"1983","unstructured":"Ben-Ari, M., Manna, Z., Pnueli, A.: The temporal logic of branching time. Acta Information\u00a020, 207\u2013226 (1983)","journal-title":"Acta Information"},{"key":"58_CR3","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: A temporal logic of concurrent programs. Theoretical Computer Science\u00a013, 45\u201360","DOI":"10.1016\/0304-3975(81)90110-9"},{"key":"58_CR4","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 Publishers, Dordrecht (1993)"},{"key":"58_CR5","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L.: Symbolic model checking: 1020 states and beyond. Information and Computation\u00a098, 142\u2013170 (1992)","journal-title":"Information and Computation"},{"key":"58_CR6","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers\u00a035, 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"58_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.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"58_CR8","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.entcs.2004.06.062","volume":"119","author":"H. Jin","year":"2005","unstructured":"Jin, H., Somenzi, F.: An incremental algorithm to check satisfiability for bounded model checking. Electronic Notes in Theoretical Computer Science\u00a0119, 51\u201365 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"58_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-27813-9_50","volume-title":"Computer Aided Verification","author":"H. Jin","year":"2004","unstructured":"Jin, H., Awedh, M., Somenzi, F.: CirCUs: A satisfiability solver geared towards bounded model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 519\u2013522. Springer, Heidelberg (2004)"},{"key":"58_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/978-3-540-30579-8_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T. Latvala","year":"2005","unstructured":"Latvala, T., Biere, A., Heljanko, K., Junttila, T.: Simple is better: Efficient bounded model checking for past LTL. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 380\u2013395. Springer, Heidelberg (2005)"},{"key":"58_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/978-3-540-30494-4_14","volume-title":"Formal Methods in Computer-Aided Design","author":"T. Latvala","year":"2004","unstructured":"Latvala, T., Biere, A., Heljanko, K., Junttila, T.: Simple bounded LTL model checking. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 186\u2013200. Springer, Heidelberg (2004)"},{"key":"58_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36126-X_15","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Frisch","year":"2002","unstructured":"Frisch, A., Sheridan, D., Walsh, T.: A fixpoint based encoding for bounded model checking. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, Springer, Heidelberg (2002)"},{"key":"58_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/3-540-44798-9_4","volume-title":"Correct Hardware Design and Verification Methods","author":"O. Shtrichman","year":"2001","unstructured":"Shtrichman, O.: Pruning techniques for the SAT-based Bounded Model Checking Problem. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol.\u00a02144, p. 58. Springer, Heidelberg (2001)"},{"key":"58_CR14","doi-asserted-by":"crossref","unstructured":"Shtrichman, O.: Tuning SAT checkers for Bounded Model-Checking. In: CAV. LNCS, vol.\u00a01855 (2000)","DOI":"10.1007\/10722167_36"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Models of Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11750321_58.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:56:47Z","timestamp":1619506607000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11750321_58"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540340218","9783540340225"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/11750321_58","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}