{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:04:15Z","timestamp":1770289455070,"version":"3.49.0"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2019,11,5]],"date-time":"2019-11-05T00:00:00Z","timestamp":1572912000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,11,5]],"date-time":"2019-11-05T00:00:00Z","timestamp":1572912000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2020,4]]},"DOI":"10.1007\/s10009-019-00547-x","type":"journal-article","created":{"date-parts":[[2019,11,5]],"date-time":"2019-11-05T14:05:13Z","timestamp":1572962713000},"page":"135-161","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["IC3 software model checking"],"prefix":"10.1007","volume":"22","author":[{"given":"Tim","family":"Lange","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin R.","family":"Neuh\u00e4u\u00dfer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Noll","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,11,5]]},"reference":[{"key":"547_CR1","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A., Gurfinkel, A., Chechik, M.: From under-approximations to over-approximations and back. In: TACAS, LNCS, vol. 7214, pp. 157\u2013172. Springer (2012)","DOI":"10.1007\/978-3-642-28756-5_12"},{"key":"547_CR2","doi-asserted-by":"crossref","unstructured":"Backeman, P., R\u00fcmmer, P., Zelji\u0107, A.: Bit-vector interpolation and quantifier elimination by lazy reduction. In: FMCAD18 (2018)","DOI":"10.23919\/FMCAD.2018.8603023"},{"key":"547_CR3","doi-asserted-by":"crossref","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: CAV, LNCS, vol. 6806, pp. 171\u2013177. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"547_CR4","doi-asserted-by":"crossref","unstructured":"Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: FMCAD, pp. 25\u201332. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"547_CR5","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: FMCAD, pp. 189\u2013197. IEEE (2010)"},{"key":"547_CR6","doi-asserted-by":"crossref","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Benchmarking and resource measurement. In: SPIN, LNCS, vol. 9232, pp. 160\u2013178. Springer (2015)","DOI":"10.1007\/978-3-319-23404-5_12"},{"key":"547_CR7","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)"},{"key":"547_CR8","doi-asserted-by":"crossref","unstructured":"Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to induction-guided abstraction-refinement (CTIGAR). In: CAV, LNCS, vol. 8559, pp. 831\u2013848. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_55"},{"key":"547_CR9","unstructured":"Bj\u00f8rner, N., Janota, M.: Playing with quantified satisfaction. In: LPAR (short papers), EPiC Series in Computing, vol.\u00a035, pp. 15\u201327. EasyChair (2015)"},{"key":"547_CR10","doi-asserted-by":"crossref","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: VMCAI, LNCS, vol. 6538, pp. 70\u201387. Springer (2011)","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"547_CR11","volume-title":"The Calculus of Computation\u2014Decision Procedures with Applications to Verification","author":"AR Bradley","year":"2007","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation\u2014Decision Procedures with Applications to Verification. Springer, Berlin (2007)"},{"key":"547_CR12","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: FMCAD, pp. 173\u2013180. IEEE (2007)","DOI":"10.1109\/FAMCAD.2007.15"},{"key":"547_CR13","unstructured":"Chockler, H., Ivrii, A., Matsliah, A., Moran, S., Nevo, Z.: Incremental formal verification of hardware. In: FMCAD, pp. 135\u2013143. FMCAD Inc. (2011)"},{"key":"547_CR14","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A.: Software model checking via IC3. In: CAV, LNCS, vol. 7358, pp. 277\u2013293. Springer (2012)","DOI":"10.1007\/978-3-642-31424-7_23"},{"key":"547_CR15","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: TACAS, LNCS, vol. 8413, pp. 46\u201361. Springer (2014)","DOI":"10.1007\/978-3-642-54862-8_4"},{"key":"547_CR16","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B., Sebastiani, R.: The MathSAT5 SMT Solver. In: TACAS, LNCS, vol. 7795. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"547_CR17","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6","volume-title":"Model Checking","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)"},{"key":"547_CR18","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"issue":"8","key":"547_CR19","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"547_CR20","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Upper Saddle River (1976)"},{"key":"547_CR21","unstructured":"E\u00e9n, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: FMCAD, pp. 125\u2013134. FMCAD Inc. (2011)"},{"key":"547_CR22","doi-asserted-by":"crossref","unstructured":"G\u00fcnther, H., Laarman, A., Weissenbacher, G.: Vienna verification tool: IC3 for parallel software (competition contribution). In: TACAS, LNCS, vol. 9636, pp. 954\u2013957. Springer (2016)","DOI":"10.1007\/978-3-662-49674-9_69"},{"key":"547_CR23","unstructured":"Gurfinkel, A., Ivrii, A.: Pushing to the top. In: FMCAD, pp. 65\u201372. IEEE (2015)"},{"key":"547_CR24","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: CAV (1), LNCS, vol. 9206, pp. 343\u2013361. Springer (2015)","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"547_CR25","doi-asserted-by":"crossref","unstructured":"Hassan, Z., Bradley, A.R., Somenzi, F.: Better generalization in IC3. In: FMCAD, pp. 157\u2013164. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679405"},{"key":"547_CR26","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370. ACM (2002)","DOI":"10.1145\/565816.503279"},{"key":"547_CR27","doi-asserted-by":"crossref","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: SAT, LNCS, vol. 7317, pp. 157\u2013171. Springer (2012)","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"547_CR28","doi-asserted-by":"crossref","unstructured":"Komuravelli, A., Bj\u00f8rner, N., Gurfinkel, A., McMillan, K.L.: Compositional verification of procedural programs using horn clauses over integers and arrays. In: FMCAD, pp. 89\u201396. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542257"},{"key":"547_CR29","doi-asserted-by":"crossref","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: CAV, LNCS, vol. 8559, pp. 17\u201334. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"547_CR30","volume-title":"Decision procedures\u2013an algorithmic point of view: Texts in theoretical computer science: An EATCS Series","author":"D Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision procedures\u2013an algorithmic point of view: Texts in theoretical computer science: An EATCS Series. Springer, Berlin (2008)"},{"key":"547_CR31","doi-asserted-by":"crossref","unstructured":"Lange, T., Neuh\u00e4u\u00dfer, M.R., Noll, T.: Speeding up the safety verification of programmable logic controller code. In: HVC, LNCS, vol. 8244, pp. 44\u201360. Springer (2013)","DOI":"10.1007\/978-3-319-03077-7_4"},{"key":"547_CR32","doi-asserted-by":"crossref","unstructured":"Lange, T., Neuh\u00e4u\u00dfer, M.R., Noll, T.: IC3 software model checking on control flow automata. In: FMCAD, pp. 97\u2013104. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542258"},{"key":"547_CR33","doi-asserted-by":"crossref","unstructured":"Lange, T., Prinz, F., Neuh\u00e4u\u00dfer, M.R., Noll, T., Katoen, J.P.: Improving generalization in software IC3. In: SPIN, LNCS, vol. 10869, pp. 85\u2013102. Springer (2018)","DOI":"10.1007\/978-3-319-94111-0_5"},{"key":"547_CR34","unstructured":"Mertens, T.: Efficient reuse of learnt information for control-flow oriented IC3 algorithms. Master thesis, RWTH Aachen University (2016)"},{"key":"547_CR35","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: TACAS, LNCS, vol. 4963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"547_CR36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Berlin (1999)"},{"key":"547_CR37","unstructured":"Prinz, F.: Generalisation methods for control-flow oriented IC3 algorithms. Master thesis, RWTH Aachen University (2016)"},{"key":"547_CR38","doi-asserted-by":"crossref","unstructured":"Tonetta, S.: Abstract model checking without computing the abstraction. In: FM, LNCS, vol. 5850, pp. 89\u2013105. Springer (2009)","DOI":"10.1007\/978-3-642-05089-3_7"},{"key":"547_CR39","unstructured":"Vojnar, T., Beyer, D.: Competition on software verification (SV-COMP). \nhttps:\/\/sv-comp.sosy-lab.org\/\n\n (2019)"},{"key":"547_CR40","doi-asserted-by":"crossref","unstructured":"Welp, T., Kuehlmann, A.: QF BV model checking with property directed reachability. In: DATE, pp. 791\u2013796. EDA Consortium (2013)","DOI":"10.7873\/DATE.2013.168"}],"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-019-00547-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-019-00547-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00547-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,4]],"date-time":"2020-11-04T00:31:03Z","timestamp":1604449863000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-019-00547-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,5]]},"references-count":40,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2020,4]]}},"alternative-id":["547"],"URL":"https:\/\/doi.org\/10.1007\/s10009-019-00547-x","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,11,5]]},"assertion":[{"value":"5 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}