{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T15:51:20Z","timestamp":1778082680554,"version":"3.51.4"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T00:00:00Z","timestamp":1648771200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T00:00:00Z","timestamp":1648771200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2022,4]]},"DOI":"10.1007\/s10703-022-00406-7","type":"journal-article","created":{"date-parts":[[2022,12,8]],"date-time":"2022-12-08T15:02:41Z","timestamp":1670511761000},"page":"117-146","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking"],"prefix":"10.1007","volume":"60","author":[{"given":"G.","family":"Cabodi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P. E.","family":"Camurati","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0605-9014","authenticated-orcid":false,"given":"M.","family":"Palena","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Pasini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,12,8]]},"reference":[{"key":"406_CR1","unstructured":"Cabodi G, Palena M, Pasini P (2014) Interpolation with guided refinement: Revisiting incrementality in sat-based unbounded model checking, In: Proceedings of the 14th conference on formal methods in computer-aided design, ser. FMCAD \u201914. Austin, TX: FMCAD Inc, pp. 12:43\u201312:50. [Online]. Available: http:\/\/dl.acm.org\/citation.cfm?id=2682923.2682938"},{"issue":"3","key":"406_CR2","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig W (1957) Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J Symbol Logic 22(3):269\u2013285","journal-title":"J Symbol Logic"},{"issue":"1","key":"406_CR3","doi-asserted-by":"publisher","first-page":"155","DOI":"10.2140\/pjm.1959.9.155","volume":"9","author":"RC Lyndon","year":"1959","unstructured":"Lyndon RC (1959) An interpolation theorem in the predicate calculus. Pacific J Math 9(1):155\u2013164","journal-title":"Pacific J Math"},{"key":"406_CR4","doi-asserted-by":"crossref","unstructured":"McMillan KL (2003) Interpolation and SAT-based model checking, In: Proceedings computer aided verification, ser. LNCS, vol. 2725. Boulder, CO, USA: Springer, pp. 1\u201313","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"406_CR5","doi-asserted-by":"crossref","unstructured":"Bradley AR (2011) Sat-based model checking without unrolling, In: VMCAI, Austin, Texas, Jan. 2011, pp. 70\u201387","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"406_CR6","unstructured":"Biere A, Jussila T The model checking competition web page, http:\/\/fmv.jku.at\/hwmcc"},{"key":"406_CR7","unstructured":"McMillan KL, Jhala R (2005) Interpolation and SAT-based model checking, In: Proceedings computer aided verification, ser. LNCS, vol. 3725. Edinburgh, Scotland, UK: Springer, pp. 39\u201351"},{"key":"406_CR8","doi-asserted-by":"crossref","unstructured":"Marques-Silva J (2005) Improvements to the implementation of Interpolant\u2013based model checking, In: Proceedings correct hardware design and verification methods, ser. LNCS, vol. 3725. Edinburgh, Scotland, UK: Springer, pp. 367\u2013370","DOI":"10.1007\/11560548_33"},{"key":"406_CR9","doi-asserted-by":"crossref","unstructured":"D\u2019Silva V, Purandare M, Kroening D (2008) Approximation refinement for interpolation-based model checking, in verification, model checking and abstract interpretation, ser. Lecture Notes in Computer Science, vol. 4905. Springer, pp. 68\u201382","DOI":"10.1007\/978-3-540-78163-9_10"},{"issue":"1","key":"406_CR10","first-page":"309","volume":"13","author":"G Cabodi","year":"2008","unstructured":"Cabodi G, Murciano M, Nocco S, Quer S (2008) Boosting interpolation with dynamic localized abstraction and redundancy removal. ACM Trans Design Autom Electr Syst 13(1):309\u2013340","journal-title":"ACM Trans Design Autom Electr Syst"},{"key":"406_CR11","doi-asserted-by":"crossref","unstructured":"Cabodi G, Camurati P, Murciano M (2008) Automated abstraction by incremental refinement in interpolant-based model checking, In: Proceedings international conference on computer-aided design. San Jose, California: ACM Press, Nov. pp. 129\u2013136","DOI":"10.1109\/ICCAD.2008.4681563"},{"key":"406_CR12","doi-asserted-by":"publisher","unstructured":"D\u2019Silva V, Kroening D, Purandare M, Weissenbacher G (2010) Interpolant strength. In: Proceedings of the 11th international conference on verification, model checking, and abstract interpretation, ser. VMCAI\u201910. Berlin, Heidelberg: Springer-Verlag, p. 129\u2013145. [Online]. Available: https:\/\/doi.org\/10.1007\/978-3-642-11319-2_12","DOI":"10.1007\/978-3-642-11319-2_12"},{"key":"406_CR13","doi-asserted-by":"crossref","unstructured":"Li B, Somenzi F (2006) Efficient abstraction refinement in interpolation-based unbounded model checking, In: Tools and algorithms for the construction and analysis of systems, vol. 3920, pp. 227\u2013241","DOI":"10.1007\/11691372_15"},{"key":"406_CR14","doi-asserted-by":"crossref","unstructured":"Cabodi G, Loiacono C, Vendraminetto D (2013) Optimization techniques for Craig interpolant compaction in unbounded model checking, In: Proceedings design automation & test in Europe conference Grenoble, France: IEEE Computer Society, Mar. pp. 1417\u20131422","DOI":"10.7873\/DATE.2013.289"},{"issue":"2","key":"406_CR15","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/s10703-015-0229-0","volume":"46","author":"G Cabodi","year":"2015","unstructured":"Cabodi G, Loiacono C, Vendraminetto D (2015) Optimization techniques for Craig interpolant compaction in unbounded model checking. Form Methods Syst Des 46(2):135\u2013162. https:\/\/doi.org\/10.1007\/s10703-015-0229-0","journal-title":"Form Methods Syst Des"},{"key":"406_CR16","doi-asserted-by":"crossref","unstructured":"Cabodi G, Camurati PE, Palena M, Pasini P, Vendraminetto D (2016) Reducing interpolant circuit size by ad-hoc logic synthesis and sat-based weakening. In: Proceedings of the 16th conference on formal methods in computer-aided design, ser. FMCAD \u201916. Austin, TX: FMCAD Inc, pp. 25\u201332. [Online]. Available: http:\/\/dl.acm.org\/citation.cfm?id=3077629.3077640","DOI":"10.1109\/FMCAD.2016.7886657"},{"key":"406_CR17","doi-asserted-by":"crossref","unstructured":"Goldberg E, G\u00fcdemann M, Kroening D, Mukherjee R (2018) Efficient verification of multi-property designs (the benefit of wrong assumptions), In: 2018 Design, automation test in Europe Conference Exhibition (DATE), pp. 43\u201348","DOI":"10.23919\/DATE.2018.8341977"},{"key":"406_CR18","doi-asserted-by":"crossref","unstructured":"Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement, In: CAV, pp. 154\u2013169","DOI":"10.1007\/10722167_15"},{"key":"406_CR19","unstructured":"Gupta A, Ganai M, Yang Z, Ashar P (2003) Iterative abstraction using SAT-based BMC with proof analysis, In: Proceedings international conference on computer-aided design, San Jose, California, Nov. pp. 416\u2013423"},{"key":"406_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 38th design automation Conference Las Vegas, Nevada: IEEE Computer Society, Jun","DOI":"10.1145\/378239.379017"},{"key":"406_CR21","unstructured":"E\u00e9n N, S\u00f6rensson N (2009) The Minisat SAT solver, http:\/\/minisat.se, Apr"},{"key":"406_CR22","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke EM, Fujita M, Zhu Y (1999) Symbolic model checking using SAT procedures instead of BDDs, In: Proceedings 36th design automation conference. New Orleans, Louisiana: IEEE Computer Society, Jun. pp. 317\u2013320","DOI":"10.1145\/309847.309942"},{"key":"406_CR23","doi-asserted-by":"crossref","unstructured":"Vizel Y, Grumberg O (2009) Interpolation-sequence based model checking. In: Proceedings formal methods in computer-aided design, ser. LNCS, vol. 2517. Austin, Texas, USA: Springer, Nov. pp. 1\u20138","DOI":"10.1109\/FMCAD.2009.5351148"},{"key":"406_CR24","doi-asserted-by":"crossref","unstructured":"Cabodi G, Nocco S, Quer S (2011) Interpolation sequences revisited. In: Proceedings design automation & test in Europe conference Grenoble, France: IEEE Computer Society, Mar. pp. 316\u2013322","DOI":"10.1109\/DATE.2011.5763056"},{"key":"406_CR25","doi-asserted-by":"crossref","unstructured":"Vizel Y, Grumberg O, Shoham S (2013) Intertwined forward-backward reachability analysis using interpolants, In: Tools and algorithms for the construction and analysis of systems, ser. LNCS, vol. 7795. Rome, Italy: Springer, Mar. pp. 308\u2013323","DOI":"10.1007\/978-3-642-36742-7_22"},{"key":"406_CR26","unstructured":"Mishchenko A, Brayton RK (2005) SAT-Based complete Don\u2019t-Care computation for network optimization, In: Proceedings design automation & test in Europe conferenece, pp. 412\u2013417"},{"issue":"5","key":"406_CR27","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2003) Counterexample-guided abstraction refinement for symbolic model checking. J ACM 50(5):752\u2013794. https:\/\/doi.org\/10.1145\/876638.876643","journal-title":"J ACM"},{"key":"406_CR28","doi-asserted-by":"publisher","unstructured":"Gupta A, Strichman O (2005) Abstraction refinement for bounded model checking. Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 112\u2013124. [Online]. Available: https:\/\/doi.org\/10.1007\/11513988_11","DOI":"10.1007\/11513988_11"},{"key":"406_CR29","unstructured":"Vizel Y, Grumberg SSO (2012) , Lazy abstraction and SAT-Based reachability in hardware model checking, In: Proceedings formal methods in computer-aided design. Cambridge, UK: IEEE, Oct. pp. 173\u2013181"},{"issue":"2","key":"406_CR30","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/s10703-011-0123-3","volume":"39","author":"G Cabodi","year":"2011","unstructured":"Cabodi G, Nocco S, Quer S (2011) Benchmarking a model checker for algorithmic improvements and tuning for performance. Formal Methods Syst Design 39(2):205\u2013227","journal-title":"Formal Methods Syst Design"},{"key":"406_CR31","doi-asserted-by":"crossref","unstructured":"Subramanyan P, Vizel Y, Ray S, Malik S (2015) Template-based synthesis of instruction-level abstractions for SOC verification, In: 2015 Formal methods in computer-aided design (FMCAD), pp. 160\u2013167","DOI":"10.1109\/FMCAD.2015.7542266"},{"key":"406_CR32","doi-asserted-by":"crossref","unstructured":"Baumgartner J, Aziz A (2003) An abstraction algorithm for the verification of level-sensitive latch-based netlists, Formal Methods in System Design, vol. 23, pp. 39\u201365, 07","DOI":"10.1023\/A:1024485130001"},{"key":"406_CR33","unstructured":"Cabodi G, Camurati P, Palena M, Pasini P\u201d (2021) , Igr - experiments, https:\/\/github.com\/P3900\/igr-exp"},{"key":"406_CR34","doi-asserted-by":"publisher","unstructured":"Vizel Y, Gurfinkel A (2014) Interpolating property directed reachability, In: Proceedings of the 16th international conference on computer aided verification - Vol. 8559. New York, NY, USA: Springer-Verlag New York, Inc., pp. 260\u2013276. [Online]. Available: https:\/\/doi.org\/10.1007\/978-3-319-08867-9_17","DOI":"10.1007\/978-3-319-08867-9_17"},{"issue":"4","key":"406_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2068716.2068720","volume":"4","author":"A Mishchenko","year":"2011","unstructured":"Mishchenko A, Brayton R, Jiang J-HR, Jang S (2011) Scalable don\u2019t-care-based logic optimization and resynthesis. ACM Trans Reconfigurable Technol Syst 4(4):1\u201323. https:\/\/doi.org\/10.1145\/2068716.2068720","journal-title":"ACM Trans Reconfigurable Technol Syst"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-022-00406-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-022-00406-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-022-00406-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,13]],"date-time":"2023-04-13T17:12:44Z","timestamp":1681405964000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-022-00406-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4]]},"references-count":35,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,4]]}},"alternative-id":["406"],"URL":"https:\/\/doi.org\/10.1007\/s10703-022-00406-7","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4]]},"assertion":[{"value":"30 July 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 November 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 December 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}