{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T04:01:21Z","timestamp":1751774481018,"version":"3.41.0"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319941103"},{"type":"electronic","value":"9783319941110"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-94111-0_5","type":"book-chapter","created":{"date-parts":[[2018,6,15]],"date-time":"2018-06-15T19:07:44Z","timestamp":1529089664000},"page":"85-102","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Improving Generalization in Software IC3"],"prefix":"10.1007","author":[{"given":"Tim","family":"Lange","sequence":"first","affiliation":[]},{"given":"Frederick","family":"Prinz","sequence":"additional","affiliation":[]},{"given":"Martin R.","family":"Neuh\u00e4u\u00dfer","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Noll","sequence":"additional","affiliation":[]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,6,16]]},"reference":[{"key":"5_CR1","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":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"831","DOI":"10.1007\/978-3-319-08867-9_55","volume-title":"Computer Aided Verification","author":"J Birgmeier","year":"2014","unstructured":"Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to induction-guided abstraction-refinement (CTIGAR). In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 831\u2013848. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_55"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7"},{"key":"5_CR4","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":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-642-31424-7_23","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2012","unstructured":"Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 277\u2013293. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_23"},{"issue":"3","key":"5_CR6","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/s10703-016-0257-4","volume":"49","author":"A Cimatti","year":"2016","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Infinite-state invariant checking with IC3 and predicate abstraction. Form. Methods Syst. Des. 49(3), 190\u2013218 (2016)","journal-title":"Form. Methods Syst. Des."},{"key":"5_CR7","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"5_CR8","unstructured":"E\u00e9n, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: FMCAD, pp. 125\u2013134. FMCAD Inc. (2011)"},{"issue":"3","key":"5_CR9","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/373243.360220","volume":"36","author":"Cormac Flanagan","year":"2001","unstructured":"Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: generating compact verification conditions. In: POPL, pp. 193\u2013205. ACM (2001)","journal-title":"ACM SIGPLAN Notices"},{"issue":"6","key":"5_CR10","doi-asserted-by":"publisher","first-page":"1026","DOI":"10.1109\/TCAD.2015.2481869","volume":"35","author":"A Griggio","year":"2016","unstructured":"Griggio, A., Roveri, M.: Comparing different variants of the IC3 algorithm for hardware model checking. IEEE Trans. CAD Integr. Circuits Syst. 35(6), 1026\u20131039 (2016)","journal-title":"IEEE Trans. CAD Integr. Circuits Syst."},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Ivrii, A.: Pushing to the top. In: FMCAD, pp. 65\u201372. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542254"},{"key":"5_CR12","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":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-31612-8_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"K Hoder","year":"2012","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157\u2013171. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_13"},{"key":"5_CR14","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"},{"issue":"6","key":"5_CR15","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/j.ipl.2004.10.015","volume":"93","author":"KRM Leino","year":"2005","unstructured":"Leino, K.R.M.: Efficient weakest preconditions. Inf. Process. Lett. 93(6), 281\u2013288 (2005)","journal-title":"Inf. Process. Lett."},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"GC Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: intermediate language and tools for analysis and transformation of C programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 213\u2013228. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45937-5_16"},{"key":"5_CR17","unstructured":"Competition on software verification (SV-COMP). https:\/\/sv-comp.sosy-lab.org\/2017\/ . Accessed 23 Jan 2017"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Visser, W., Geldenhuys, J., Dwyer, M.B.: Green: reducing, reusing and recycling constraints in program analysis. In: SIGSOFT FSE, p. 58. ACM (2012)","DOI":"10.1145\/2393596.2393665"},{"key":"5_CR19","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":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94111-0_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T04:30:58Z","timestamp":1751689858000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94111-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319941103","9783319941110"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94111-0_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}