{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,2]],"date-time":"2025-07-02T11:47:34Z","timestamp":1751456854983},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2005,2,15]],"date-time":"2005-02-15T00:00:00Z","timestamp":1108425600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2005,4]]},"DOI":"10.1007\/s10009-004-0182-5","type":"journal-article","created":{"date-parts":[[2005,2,14]],"date-time":"2005-02-14T13:17:58Z","timestamp":1108387078000},"page":"174-183","source":"Crossref","is-referenced-by-count":23,"title":["Computational challenges in bounded model checking"],"prefix":"10.1007","volume":"7","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","published-online":{"date-parts":[[2005,2,15]]},"reference":[{"key":"182_CR1","unstructured":"Ajtai M, Koml\u00f3s J, Szemer\u00e9di S (1983) An O(NlogN) sorting network. In: Proceedings of the 25th ACM symposium on theory of computing, pp 1\u20139"},{"key":"182_CR2","doi-asserted-by":"crossref","unstructured":"Batcher KE (1968) Sorting networks and their applications. In: Proceedings of the AFIPS spring joint computer conference, 32:307\u2013314","DOI":"10.1145\/1468075.1468121"},{"key":"182_CR3","doi-asserted-by":"crossref","unstructured":"Baumgartner J, Kuehlmann A, Abraham J (2002) Property checking via structural analysis. In: Brinksma E, Larsen KG (eds) Proceedings of the 14th international conference on computer aided verification (CAV\u201902), Copenhagen, Denmark, July 2002. Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York","DOI":"10.1007\/3-540-45657-0_12"},{"key":"182_CR4","unstructured":"Biere A (2004) The evolution from limmat to nanosat. Technical report, ETH Z\u00fcrich"},{"key":"182_CR5","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke E, Zhu Y (1999) Symbolic model checking without BDDs. In: Proceedings of the workshop on tools and algorithms for the construction and analysis of systems (TACAS\u201999). Lecture notes in computer science, vol . Springer, Berlin Heidelberg New York, pp 193\u2013207","DOI":"10.1007\/3-540-49059-0_14"},{"key":"182_CR6","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke EM, Strichman O, Zue Y (2003) Bounded model checking. In: Advances in computers, vol 58. Academic, New York","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"182_CR7","doi-asserted-by":"crossref","unstructured":"Cimatti A, Pistore M, Roveri M, Sebastiani R (2002) Improving the encoding of LTL model checking into SAT. In: 3rd international conference on verification, model checking and abstract interpretation (VMCAI), pp 196\u2013207","DOI":"10.1007\/3-540-47813-2_14"},{"key":"182_CR8","doi-asserted-by":"crossref","unstructured":"Clarke EM, Grumberg O, Hamaguchi K (1994) Another look at ltl model checking. In: Dill DL (ed) Proceedings of the 6th international conference on computer aided verification. Lecture notes in computer science, vol 818. Springer, Berlin Heidelberg New York, pp 415\u2013427","DOI":"10.1007\/3-540-58179-0_72"},{"key":"182_CR9","doi-asserted-by":"crossref","unstructured":"Clarke EM, Kroening D, Ouaknine J, Strichman O (2004) Completeness and complexity of bounded model checking. In: Proceedings of the 5th international conference on verification, model checking and abstract interpretation (VMCAI\u201904), Venice, Italy, January 2004. Lecture notes in computer science, vol 2937. Springer, Berlin Heidelberg New York, pp 85\u201396","DOI":"10.1007\/978-3-540-24622-0_9"},{"key":"182_CR10","doi-asserted-by":"crossref","unstructured":"de Moura L, Ruess H, Sorea M (2002) Lazy theorem proving for bounded model checking over infinite domains. In: Proceedings of the 18th international conference on automated deduction (CADE\u201902), Copenhagen, July 2002","DOI":"10.1007\/3-540-45620-1_35"},{"key":"182_CR11","unstructured":"Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge, MA"},{"key":"182_CR12","doi-asserted-by":"crossref","unstructured":"Frisch A, Sheridan D, Walsh T (2002) A fixpoint based encoding for bounded model checking. In: International conference on formal methods in computer-aided design (FMCAD 2002), Portland, OR, November, pp 238\u2013255","DOI":"10.1007\/3-540-36126-X_15"},{"key":"182_CR13","unstructured":"Gerth R, Peled D, Vardi M, Wolper P (1995) Simple on-the-fly automatic verification of linear temporal logic. In: Protocol specification testing and verification. Chapman & Hall, London, pp 3\u201318"},{"key":"182_CR14","unstructured":"Holzmann GJ, Peled D, Yannakakis M (1996) On nested depth first search. In: 2nd SPIN workshop, AMS, pp 23\u201332"},{"key":"182_CR15","unstructured":"Knuth DE (1973) The art of computer programming, vol 3: Sorting and searching. Addison-Wesley, Reading, MA"},{"key":"182_CR16","doi-asserted-by":"crossref","unstructured":"Kroening D, Strichman O (2003) Efficient computation of recurrence diameters. In: Proceedings of the 4th international conference on verification, model checking, and abstract interpretation (VMCAI\u201903), New York, January 2003. Lecture notes in computer science, vol 2575. Springer, Berlin Heidelberg New York, pp 298\u2013309","DOI":"10.1007\/3-540-36384-X_24"},{"key":"182_CR17","doi-asserted-by":"crossref","unstructured":"McMillan KL (2002) Applying SAT methods in unbounded symbolic model checking. In: Brinksma E, Larsen K (eds) Proceedings of the 14th international conference on computer aided verification (CAV\u201902), Copenhagen, July 2002. Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York, pp 250\u2013264","DOI":"10.1007\/3-540-45657-0_19"},{"key":"182_CR18","doi-asserted-by":"crossref","unstructured":"McMillan KL (2003) Interpolation and sat-based model checking. In: Hunt WA Jr, Somenzi F (eds) Proceedings of the international conference on computer aided verification (CAV\u201903), July 2003. Lecture notes in computer science, vol . Springer, Berlin Heidelberg New York","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"182_CR19","doi-asserted-by":"crossref","unstructured":"Mneimneh M, Sakallah K (2002) SAT-based sequential depth computation. In: Workshop on constraints in formal verification, Ithaca, New York, September","DOI":"10.1145\/1119772.1119790"},{"key":"182_CR20","doi-asserted-by":"crossref","unstructured":"Moskewicz M, Madigan C, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient SAT solver. In: Proceedings of the conference on design automation (DAC\u201901)","DOI":"10.1145\/378239.379017"},{"key":"182_CR21","doi-asserted-by":"crossref","unstructured":"Schuppan V, Biere A (2004) Efficient reduction of finite state model checking to reachability analysis. Int J Softw Tools Technol Transfer","DOI":"10.1007\/s10009-003-0121-x"},{"key":"182_CR22","doi-asserted-by":"crossref","unstructured":"Sheeran M, Singh S, Stalmarck G (2000) Checking safety properties using induction and a sat-solver. In: Hunt, Johnson (eds) Proceedings of the international conference on formal methods in computer-aided design (FMCAD 2000)","DOI":"10.1007\/3-540-40922-X_8"},{"key":"182_CR23","doi-asserted-by":"crossref","unstructured":"Somenzi F, Bloem R (2000) Efficient B\u00fcchi automata from LTL formulae. In: Emerson EA, Sistla AP (eds) 12th international conference on computer aided verification (CAV\u201900), Berlin, July. Springer, Berlin Heidelberg New York, pp 248\u2013263","DOI":"10.1007\/10722167_21"},{"key":"182_CR24","unstructured":"Vardi MY, Wolper P (1986) An automata-theoretic approach to automatic program verification. In: Proceedings of the 1st IEEE symposium on logic in computer science, pp 332\u2013344"},{"key":"182_CR25","doi-asserted-by":"crossref","unstructured":"Wang D, Clarke EM, Zhu Y, Kukula J (2001) Using cutwidth to improve symbolic simulation and boolean satisfiability. In: IEEE International workshop on high level design validation and test (HLDVT 2001), November, p 6","DOI":"10.1109\/HLDVT.2001.972824"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0182-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-004-0182-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0182-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,5]],"date-time":"2020-04-05T19:34:29Z","timestamp":1586115269000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-004-0182-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,2,15]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,4]]}},"alternative-id":["182"],"URL":"https:\/\/doi.org\/10.1007\/s10009-004-0182-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,2,15]]}}}