{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:55:17Z","timestamp":1725551717830},"publisher-location":"Berlin, Heidelberg","reference-count":19,"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_14","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T18:42:14Z","timestamp":1277836934000},"page":"186-200","source":"Crossref","is-referenced-by-count":30,"title":["Simple Bounded LTL Model Checking"],"prefix":"10.1007","author":[{"given":"Timo","family":"Latvala","sequence":"first","affiliation":[]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[]},{"given":"Keijo","family":"Heljanko","sequence":"additional","affiliation":[]},{"given":"Tommi","family":"Junttila","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","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":"14_CR2","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/B:FORM.0000004785.67232.f8","volume":"24","author":"O. Strichman","year":"2004","unstructured":"Strichman, O.: Accelerating bounded model checking of safety properties. Formal Methods in System Design\u00a024, 5\u201324 (2004)","journal-title":"Formal Methods in System Design"},{"key":"14_CR3","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. Kroenig","year":"2002","unstructured":"Kroenig, 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":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-540-24622-0_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroenig, D., Oukanine, J., Strichman, O.: Completeness and complexity of bounded model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 85\u201396. Springer, Heidelberg (2004)"},{"key":"14_CR5","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":"14_CR6","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 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)"},{"key":"14_CR7","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.: Model checking of safety properties. Formal Methods in System Design\u00a019, 291\u2013314 (2001)","journal-title":"Formal Methods in System Design"},{"key":"14_CR8","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s100090200070","volume":"4","author":"H. Tauriainen","year":"2002","unstructured":"Tauriainen, H., Heljanko, K.: Testing LTL formula translation into B\u00fcchi automata. STTT - International Journal on Software Tools for Technology Transfer\u00a04, 57\u201370 (2002)","journal-title":"STTT - International Journal on Software Tools for Technology Transfer"},{"key":"14_CR9","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"14_CR10","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BF01383878","volume":"2","author":"R. Cleaveland","year":"1993","unstructured":"Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Formal Methods in System Desing\u00a02, 121\u2013147 (1993)","journal-title":"Formal Methods in System Desing"},{"key":"14_CR11","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1017\/S1471068403001790","volume":"3","author":"K. Heljanko","year":"2003","unstructured":"Heljanko, K., Niemel\u00e4, I.: Bounded LTL model checking with stable models. Theory and Practice of Logic Programming\u00a03, 519\u2013550 (2003)","journal-title":"Theory and Practice of Logic Programming"},{"key":"14_CR12","unstructured":"Janhunen, T.: A counter-based approach to translating logic programs into set of clauses. In: Proceedings of the 2nd International Workshop on Answer Set Programming (ASP 2003), Sun SITE Central Europe (CEUR), vol.\u00a078, pp. 166\u2013180 (2003)"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"14_CR14","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. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 438\u2013455. Springer, Heidelberg (2002)"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Schuppan, V., Biere, A.: Efficient reduction of finite state model checking to reachability analysis. Software Tools for Technology Transfer (STTT)\u00a05 (2004)","DOI":"10.1007\/s10009-003-0121-x"},{"key":"14_CR16","doi-asserted-by":"crossref","first-page":"824","DOI":"10.1145\/775832.776040","volume-title":"Proceedings of the 40th Conference on Design Automation","author":"A. Gupta","year":"2003","unstructured":"Gupta, A., Ganai, M., Wang, C., Yang, Z., Ashar, P.: Learning from BDDs in SAT-based bounded model checking. In: Proceedings of the 40th Conference on Design Automation, pp. 824\u2013829. IEEE, Los Alamitos (2003)"},{"key":"14_CR17","unstructured":"Jackson, P., Sheridan, D.: The optimality of a fast CNF conversion and its use with SAT. Technical Report APES-82-2004, APES Research Group (2004), Available from http:\/\/www.dcs.st-and.ac.uk\/apes\/apesreports.html"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (2001)","DOI":"10.1145\/378239.379017"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-36577-X_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Benedetti","year":"2003","unstructured":"Benedetti, M., Cimatti, A.: Bounded model checking for past LTL. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 18\u201333. Springer, Heidelberg (2003)"}],"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_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,30]],"date-time":"2021-10-30T10:06:00Z","timestamp":1635588360000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30494-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540237389","9783540304944"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30494-4_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}