{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T10:37:45Z","timestamp":1761561465980},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540208037"},{"type":"electronic","value":"9783540246220"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24622-0_9","type":"book-chapter","created":{"date-parts":[[2010,9,5]],"date-time":"2010-09-05T11:33:53Z","timestamp":1283686433000},"page":"85-96","source":"Crossref","is-referenced-by-count":59,"title":["Completeness and Complexity of Bounded Model Checking"],"prefix":"10.1007","author":[{"given":"Edmund","family":"Clarke","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]},{"given":"Jo\u00ebl","family":"Ouaknine","sequence":"additional","affiliation":[]},{"given":"Ofer","family":"Strichman","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/3-540-45657-0_12","volume-title":"Computer Aided Verification","author":"J. Baumgartner","year":"2002","unstructured":"Baumgartner, J., Kuehlmann, A., Abraham, J.: Property checking via structural analysis. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 151. Springer, Heidelberg (2002)"},{"key":"9_CR2","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":"9_CR3","series-title":"Advances in computers","volume-title":"Bounded Model Checking","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zue, Y.: Bounded Model Checking. Advances in computers, vol.\u00a058. Academic Press, London (2003)"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/3-540-47813-2_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Pistore, M., Roveri, M., Sebastiani, R.: Improving the encoding of LTL model checking into SAT. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol.\u00a02294, pp. 196\u2013207. Springer, Heidelberg (2002)"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/3-540-58179-0_72","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at ltl model checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 415\u2013427. Springer, Heidelberg (1994)"},{"key":"9_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1007\/3-540-45620-1_35","volume-title":"Automated Deduction - CADE-18","author":"L. Moura de","year":"2002","unstructured":"de Moura, L., Rue\u00df, H., Sorea, M.: Lazy theorem proving for bounded model checking over infinite domains. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, p. 438. Springer, Heidelberg (2002)"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","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, pp. 238\u2013255. Springer, Heidelberg (2002)"},{"doi-asserted-by":"crossref","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proc. 7th ACM Symp. Princ. of Prog. Lang., pp. 163\u2013173 (1980)","key":"9_CR8","DOI":"10.1145\/567446.567462"},{"key":"9_CR9","first-page":"3","volume-title":"Protocol Specification Testing and Verification","author":"R. Gerth","year":"1995","unstructured":"Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification Testing and Verification, pp. 3\u201318. Chapman & Hall, Boca Raton (1995)"},{"key":"9_CR10","first-page":"23","volume-title":"Second SPIN workshop","author":"G.J. Holzmann","year":"1996","unstructured":"Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth first search. In: Second SPIN workshop, pp. 23\u201332. AMS, Providence (1996)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/3-540-36384-X_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Kroening","year":"2002","unstructured":"Kroening, D., Strichman, O.: Efficient computation of recurrence diameters. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 298\u2013309. Springer, Heidelberg (2002)"},{"key":"9_CR12","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1991)"},{"doi-asserted-by":"crossref","unstructured":"Mneimneh, M., Sakallah, K.: SAT-based sequential depth computation. In: Constraints in formal verification workshop, Ithaca, New York (September 2002)","key":"9_CR13","DOI":"10.1145\/1119772.1119790"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification","author":"F. Somenzi","year":"2000","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 248\u2013263. Springer, Heidelberg (2000)"},{"unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. First IEEE Symp. Logic in Comp. Sci., pp. 332\u2013344 (1986)","key":"9_CR15"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24622-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,3]],"date-time":"2019-06-03T17:40:44Z","timestamp":1559583644000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24622-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208037","9783540246220"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24622-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}