{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:21:17Z","timestamp":1779074477632,"version":"3.51.4"},"reference-count":63,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2025,2,5]],"date-time":"2025-02-05T00:00:00Z","timestamp":1738713600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,2,5]],"date-time":"2025-02-05T00:00:00Z","timestamp":1738713600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005722","name":"Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005722","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The article <jats:italic>Interpolation and SAT-Based Model Checking<\/jats:italic> (McMillan in: Proc. CAV 2003, LNCS, Springer [56]) describes a formal-verification algorithm, which was originally devised to verify safety properties of finite-state transition systems. It derives interpolants from unsatisfiable BMC queries and collects them to construct an overapproximation of the set of reachable states. Although 20\u00a0years old, the algorithm is still state-of-the-art in hardware model checking. Unlike other formal-verification algorithms, such as \"Image missing\" or PDR, which have been extended to handle infinite-state systems and investigated for program analysis, McMillan\u2019s interpolation-based model-checking algorithm from 2003 has not been used to verify programs so far. Our contribution is to close this significant, two decades old gap in knowledge by adopting the algorithm to software verification. We implemented it in the verification framework CPA<jats:sc>checker<\/jats:sc> and evaluated the implementation against other state-of-the-art software-verification techniques on the largest publicly available benchmark suite of C\u00a0safety-verification tasks. The evaluation demonstrates that McMillan\u2019s interpolation-based model-checking algorithm from 2003 is competitive among other algorithms in terms of both the number of solved verification tasks and the run-time efficiency. Our results are important for the area of software verification, because researchers and developers now have one more approach to choose from.<\/jats:p>","DOI":"10.1007\/s10817-024-09702-9","type":"journal-article","created":{"date-parts":[[2025,2,5]],"date-time":"2025-02-05T08:02:14Z","timestamp":1738742534000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification"],"prefix":"10.1007","volume":"69","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4832-7662","authenticated-orcid":false,"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8096-5595","authenticated-orcid":false,"given":"Nian-Ze","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5139-341X","authenticated-orcid":false,"given":"Philipp","family":"Wendler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,2,5]]},"reference":[{"key":"9702_CR1","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley, Boston (1986). https:\/\/www.worldcat.org\/isbn\/978-0-201-10088-4"},{"key":"9702_CR2","doi-asserted-by":"publisher","unstructured":"Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: Ufo: A framework for abstraction- and interpolation-based software verification. In: Proc. CAV, LNCS\u00a07358, pp. 672\u2013678. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_48","DOI":"10.1007\/978-3-642-31424-7_48"},{"key":"9702_CR3","doi-asserted-by":"publisher","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: An extension of lazy abstraction with interpolation for programs with arrays. Form. Methods Syst. Des. 45(1), 63\u2013109 (2014). https:\/\/doi.org\/10.1007\/s10703-014-0209-9","DOI":"10.1007\/s10703-014-0209-9"},{"key":"9702_CR4","doi-asserted-by":"publisher","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S.K.: Slam and Static Driver Verifier: Technology transfer of formal methods inside Microsoft. In: Proc. IFM, LNCS\u00a02999, pp. 1\u201320. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24756-2_1","DOI":"10.1007\/978-3-540-24756-2_1"},{"key":"9702_CR5","doi-asserted-by":"publisher","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proc. PLDI, pp. 203\u2013213. ACM (2001). https:\/\/doi.org\/10.1145\/378795.378846","DOI":"10.1145\/378795.378846"},{"key":"9702_CR6","doi-asserted-by":"publisher","unstructured":"Ball, T., Rajamani, S.K.: The Slam project: Debugging system software via static analysis. In: Proc. POPL, pp. 1\u20133. ACM (2002). https:\/\/doi.org\/10.1145\/503272.503274","DOI":"10.1145\/503272.503274"},{"key":"9702_CR7","doi-asserted-by":"publisher","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Model Checking, pp. 305\u2013343. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"9702_CR8","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Progress on software verification: SV-COMP 2022. In: Proc. TACAS\u00a0(2), LNCS\u00a013244, pp. 375\u2013402. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_20","DOI":"10.1007\/978-3-030-99527-0_20"},{"key":"9702_CR9","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5831003","author":"D Beyer","year":"2022","unstructured":"Beyer, D.: SV-Benchmarks: Benchmark set for software verification and testing (SV-COMP 2022 and Test-Comp 2022). Zenodo (2022). https:\/\/doi.org\/10.5281\/zenodo.5831003","journal-title":"Zenodo"},{"key":"9702_CR10","doi-asserted-by":"publisher","unstructured":"Beyer, D., Chien, P.C., Lee, N.Z.: CPA-DF: A tool for configurable interval analysis to boost program verification. In: Proc. ASE, pp. 2050\u20132053. IEEE (2023). https:\/\/doi.org\/10.1109\/ASE56229.2023.00213","DOI":"10.1109\/ASE56229.2023.00213"},{"key":"9702_CR11","doi-asserted-by":"publisher","unstructured":"Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: Proc. FMCAD, pp. 25\u201332. IEEE (2009). https:\/\/doi.org\/10.1109\/FMCAD.2009.5351147","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"9702_CR12","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M.: Software verification with PDR: An implementation of the state of the art. In: Proc. TACAS\u00a0(1), LNCS\u00a012078, pp. 3\u201321. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_1","DOI":"10.1007\/978-3-030-45190-5_1"},{"key":"9702_CR13","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction with continuously-refined invariants. In: Proc. CAV, LNCS\u00a09206, pp. 622\u2013640. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_42","DOI":"10.1007\/978-3-319-21690-4_42"},{"issue":"3","key":"9702_CR14","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/s10817-017-9432-6","volume":"60","author":"D Beyer","year":"2018","unstructured":"Beyer, D., Dangl, M., Wendler, P.: A unifying view on SMT-based software verification. J. Autom. Reason. 60(3), 299\u2013335 (2018). https:\/\/doi.org\/10.1007\/s10817-017-9432-6","journal-title":"J. Autom. Reason."},{"key":"9702_CR15","doi-asserted-by":"publisher","unstructured":"Beyer, D., Gulwani, S., Schmidt, D.: Combining model checking and data-flow analysis. In: Handbook of Model Checking, pp. 493\u2013540. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_16","DOI":"10.1007\/978-3-319-10575-8_16"},{"issue":"5\u20136","key":"9702_CR16","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. Int. J. Softw. Tools Technol. Transf. 9(5\u20136), 505\u2013525 (2007). https:\/\/doi.org\/10.1007\/s10009-007-0044-z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"9702_CR17","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Configurable software verification: Concretizing the convergence of model checking and program analysis. In: Proc. CAV, LNCS\u00a04590, pp. 504\u2013518. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_51","DOI":"10.1007\/978-3-540-73368-3_51"},{"key":"9702_CR18","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Program analysis with dynamic precision adjustment. In: Proc. ASE, pp. 29\u201338. IEEE (2008). https:\/\/doi.org\/10.1109\/ASE.2008.13","DOI":"10.1109\/ASE.2008.13"},{"key":"9702_CR19","doi-asserted-by":"publisher","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Proc. CAV, LNCS\u00a06806, pp. 184\u2013190. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"9702_CR20","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Proc. FMCAD, pp. 189\u2013197. FMCAD (2010). https:\/\/ieeexplore.ieee.org\/document\/5770949"},{"key":"9702_CR21","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8245824","author":"D Beyer","year":"2023","unstructured":"Beyer, D., Lee, N.Z., Wendler, P.: Reproduction package for article \u2018Interpolation and SAT-based model checking revisited\u2019. Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.8245824","journal-title":"Zenodo"},{"issue":"1","key":"9702_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-017-0469-y","volume":"21","author":"D Beyer","year":"2019","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: requirements and solutions. Int. J. Softw. Tools Technol. Transf. 21(1), 1\u201329 (2019). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"9702_CR23","doi-asserted-by":"publisher","unstructured":"Beyer, D., Petrenko, A.K.: Linux driver verification. In: Proc. ISoLA, LNCS\u00a07610, pp. 1\u20136. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-34032-1_1","DOI":"10.1007\/978-3-642-34032-1_1"},{"key":"9702_CR24","doi-asserted-by":"publisher","unstructured":"Beyer, D., Zufferey, D., Majumdar, R.: CSIsat: Interpolation for LA+EUF. In: Proc. CAV, LNCS\u00a05123, pp. 304\u2013308. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_29","DOI":"10.1007\/978-3-540-70545-1_29"},{"key":"9702_CR25","doi-asserted-by":"publisher","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proc. TACAS, LNCS\u00a01579, pp. 193\u2013207. Springer (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"key":"9702_CR26","doi-asserted-by":"publisher","unstructured":"Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to induction-guided abstraction-refinement (CTIGAR). In: Proc. CAV, LNCS\u00a08559, pp. 831\u2013848. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_55","DOI":"10.1007\/978-3-319-08867-9_55"},{"key":"9702_CR27","doi-asserted-by":"publisher","unstructured":"Blicha, M., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: Transition power abstractions for deep counterexample detection. In: Proc. TACAS, LNCS\u00a013243, pp. 524\u2013542. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_29","DOI":"10.1007\/978-3-030-99524-9_29"},{"key":"9702_CR28","doi-asserted-by":"publisher","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Proc. VMCAI, LNCS\u00a06538, pp. 70\u201387. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"9702_CR29","doi-asserted-by":"publisher","unstructured":"Br\u00fcckner, I., Dr\u00e4ger, K., Finkbeiner, B., Wehrheim, H.: Slicing abstractions. In: Proc. FSEN, LNCS\u00a04767, pp. 17\u201332. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-75698-9_2","DOI":"10.1007\/978-3-540-75698-9_2"},{"key":"9702_CR30","doi-asserted-by":"publisher","unstructured":"Cabodi, G., Nocco, S., Quer, S.: Interpolation sequences revisited. In: Proc. DATE, pp. 1\u20136. IEEE (2011). https:\/\/doi.org\/10.1109\/DATE.2011.5763056","DOI":"10.1109\/DATE.2011.5763056"},{"key":"9702_CR31","doi-asserted-by":"publisher","unstructured":"Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M., O\u2019Hearn, P.W., Papakonstantinou, I., Purbrick, J., Rodriguez, D.: Moving fast with software verification. In: Proc. NFM, LNCS\u00a09058, pp. 3\u201311. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_1","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"9702_CR32","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A.: Software model checking via IC3. In: Proc. CAV, LNCS\u00a07358, pp. 277\u2013293. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_23","DOI":"10.1007\/978-3-642-31424-7_23"},{"key":"9702_CR33","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Proc. TACAS, LNCS\u00a07795, pp. 93\u2013107. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7","DOI":"10.1007\/978-3-642-36742-7_7"},{"issue":"5","key":"9702_CR34","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003). https:\/\/doi.org\/10.1145\/876638.876643","journal-title":"J. ACM"},{"key":"9702_CR35","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Kr\u00f6ning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Proc. TACAS, LNCS\u00a02988, pp. 168\u2013176. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"9702_CR36","doi-asserted-by":"publisher","unstructured":"Cook, B.: Formal reasoning about the security of Amazon web services. In: Proc. CAV\u00a0(2), LNCS\u00a010981, pp. 38\u201347. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_3","DOI":"10.1007\/978-3-319-96145-3_3"},{"key":"9702_CR37","doi-asserted-by":"publisher","unstructured":"Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J.\u00a0Symb. Log. 22(3), 250\u2013268 (1957). https:\/\/doi.org\/10.2307\/2963593","DOI":"10.2307\/2963593"},{"key":"9702_CR38","doi-asserted-by":"publisher","unstructured":"Donaldson, A.F., Haller, L., Kr\u00f6ning, D., R\u00fcmmer, P.: Software verification using k-induction. In: Proc. SAS, LNCS\u00a06887, pp. 351\u2013368. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-23702-7_26","DOI":"10.1007\/978-3-642-23702-7_26"},{"issue":"1","key":"9702_CR39","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s10703-011-0124-2","volume":"39","author":"AF Donaldson","year":"2011","unstructured":"Donaldson, A.F., Kr\u00f6ning, D., R\u00fcmmer, P.: Automatic analysis of DMA races using model checking and k-induction. FMSD 39(1), 83\u2013113 (2011). https:\/\/doi.org\/10.1007\/s10703-011-0124-2","journal-title":"FMSD"},{"key":"9702_CR40","doi-asserted-by":"publisher","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: Proc. POPL, pp. 191\u2013202. ACM (2002). https:\/\/doi.org\/10.1145\/503272.503291","DOI":"10.1145\/503272.503291"},{"key":"9702_CR41","doi-asserted-by":"publisher","unstructured":"Ghilardi, S., Ranise, S.: Goal-directed invariant synthesis for model checking modulo theories. In: Proc. TABLEAUX, LNCS\u00a05607, pp. 173\u2013188. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-02716-1_14","DOI":"10.1007\/978-3-642-02716-1_14"},{"key":"9702_CR42","doi-asserted-by":"publisher","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with Pvs. In: Proc. CAV, LNCS\u00a01254, pp. 72\u201383. Springer (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_10","DOI":"10.1007\/3-540-63166-6_10"},{"key":"9702_CR43","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: Proc. SAS, LNCS\u00a05673, pp. 69\u201385. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-03237-0_7","DOI":"10.1007\/978-3-642-03237-0_7"},{"key":"9702_CR44","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Proc. CAV, LNCS\u00a08044, pp. 36\u201352. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_2","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"9702_CR45","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Proc. POPL, pp. 232\u2013244. ACM (2004). https:\/\/doi.org\/10.1145\/964001.964021","DOI":"10.1145\/964001.964021"},{"key":"9702_CR46","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. POPL, pp. 58\u201370. ACM (2002). https:\/\/doi.org\/10.1145\/503272.503279","DOI":"10.1145\/503272.503279"},{"key":"9702_CR47","doi-asserted-by":"publisher","unstructured":"Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D.: The RERS grey-box challenge 2012: Analysis of event-condition-action systems. In: Proc. ISoLA, LNCS\u00a07609, pp. 608\u2013614. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-34026-0_45","DOI":"10.1007\/978-3-642-34026-0_45"},{"key":"9702_CR48","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592438","author":"R Jhala","year":"2009","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. (2009). https:\/\/doi.org\/10.1145\/1592434.1592438","journal-title":"ACM Comput. Surv."},{"key":"9702_CR49","doi-asserted-by":"publisher","unstructured":"Jhala, R., McMillan, K.L.: Interpolant-based transition relation approximation. In: Proc. CAV, LNCS\u00a03576, pp. 39\u201351. Springer (2005). https:\/\/doi.org\/10.1007\/11513988_6","DOI":"10.1007\/11513988_6"},{"key":"9702_CR50","doi-asserted-by":"publisher","unstructured":"Jovanovic, D., Dutertre, B.: Property-directed k-induction. In: Proc. FMCAD, pp. 85\u201392. IEEE (2016). https:\/\/doi.org\/10.1109\/FMCAD.2016.7886665","DOI":"10.1109\/FMCAD.2016.7886665"},{"key":"9702_CR51","doi-asserted-by":"publisher","unstructured":"Kahsai, T., Tinelli, C.: PKind: A parallel k-induction based model checker. In: Proc. Int. Workshop on Parallel and Distributed Methods in Verification, EPTCS\u00a072, pp. 55\u201362. EPTCS (2011). https:\/\/doi.org\/10.4204\/EPTCS.72.6","DOI":"10.4204\/EPTCS.72.6"},{"key":"9702_CR52","doi-asserted-by":"publisher","unstructured":"Khoroshilov, A.V., Mutilin, V.S., Petrenko, A.K., Zakharov, V.: Establishing Linux driver verification process. In: Proc. Ershov Memorial Conference, LNCS\u00a05947, pp. 165\u2013176. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-11486-1_14","DOI":"10.1007\/978-3-642-11486-1_14"},{"key":"9702_CR53","doi-asserted-by":"publisher","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic abstraction in SMT-based unbounded software model checking. In: Proc. CAV, LNCS\u00a08044, pp. 846\u2013862. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_59","DOI":"10.1007\/978-3-642-39799-8_59"},{"key":"9702_CR54","doi-asserted-by":"publisher","unstructured":"Kr\u00f6ning, D., Weissenbacher, G.: Interpolation-based software verification with Wolverine. In: Proc. CAV, LNCS\u00a06806, pp. 573\u2013578. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_45","DOI":"10.1007\/978-3-642-22110-1_45"},{"key":"9702_CR55","doi-asserted-by":"publisher","unstructured":"Lange, T., Neuh\u00e4u\u00dfer, M.R., Noll, T.: IC3 software model checking on control flow automata. In: Proc. FMCAD, pp. 97\u2013104 (2015). https:\/\/doi.org\/10.1109\/FMCAD.2015.7542258","DOI":"10.1109\/FMCAD.2015.7542258"},{"key":"9702_CR56","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Proc. CAV, LNCS\u00a02725, pp. 1\u201313. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"9702_CR57","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Proc. CAV, LNCS\u00a04144, pp. 123\u2013136. Springer (2006). https:\/\/doi.org\/10.1007\/11817963_14","DOI":"10.1007\/11817963_14"},{"key":"9702_CR58","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Lazy annotation for program testing and verification. In: Proc. CAV, LNCS\u00a06174, pp. 104\u2013118. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_10","DOI":"10.1007\/978-3-642-14295-6_10"},{"key":"9702_CR59","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Interpolation and model checking. In: Handbook of Model Checking, pp. 421\u2013446. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_14","DOI":"10.1007\/978-3-319-10575-8_14"},{"key":"9702_CR60","unstructured":"McMillan, K.L., Rybalchenko, A.: Computing relational fixed points using interpolation. Tech. Rep. https:\/\/www.microsoft.com\/en-us\/research\/publication\/computing-relational-fixed-points-using-interpolation\/, Microsoft Research (2013)"},{"key":"9702_CR61","doi-asserted-by":"publisher","unstructured":"Sery, O., Fedyukovich, G., Sharygina, N.: Interpolation-based function summaries in bounded model checking. In: Proc. HVC, LNCS\u00a07261, pp. 160\u2013175. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-34188-5_15","DOI":"10.1007\/978-3-642-34188-5_15"},{"key":"9702_CR62","doi-asserted-by":"publisher","unstructured":"Vizel, Y., Grumberg, O.: Interpolation-sequence based model checking. In: Proc. FMCAD, pp. 1\u20138. IEEE (2009). https:\/\/doi.org\/10.1109\/FMCAD.2009.5351148","DOI":"10.1109\/FMCAD.2009.5351148"},{"issue":"1","key":"9702_CR63","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1134\/S0361768815010065","volume":"41","author":"IS Zakharov","year":"2015","unstructured":"Zakharov, I.S., Mandrykin, M.U., Mutilin, V.S., Novikov, E., Petrenko, A.K., Khoroshilov, A.V.: Configurable toolset for static verification of operating systems kernel modules. Program. Comp. Softw. 41(1), 49\u201364 (2015). https:\/\/doi.org\/10.1134\/S0361768815010065","journal-title":"Program. Comp. Softw."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09702-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-024-09702-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09702-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T20:53:33Z","timestamp":1742676813000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-024-09702-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,2,5]]},"references-count":63,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,3]]}},"alternative-id":["9702"],"URL":"https:\/\/doi.org\/10.1007\/s10817-024-09702-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,2,5]]},"assertion":[{"value":"11 August 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 July 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 February 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"5"}}