{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T03:51:37Z","timestamp":1742961097738,"version":"3.40.3"},"publisher-location":"Cham","reference-count":59,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031661488"},{"type":"electronic","value":"9783031661495"}],"license":[{"start":{"date-parts":[[2024,10,13]],"date-time":"2024-10-13T00:00:00Z","timestamp":1728777600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,10,13]],"date-time":"2024-10-13T00:00:00Z","timestamp":1728777600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"Abstract<\/jats:title>Software model checking is a challenging problem, and generating relevant invariants is a key factor in proving the safety properties of a program. Program invariants can be obtained by various approaches, including lightweight procedures based on data-flow analysis and intensive techniques using Craig interpolation. Although data-flow analysis runs efficiently, it often produces invariants that are too weak to prove the properties. By contrast, interpolation-based approaches build strong invariants from interpolants, but they might not scale well due to expensive interpolation procedures. Invariants can also be injected into model-checking algorithms to assist the analysis. Invariant injection has been studied for many well-known approaches, including k<\/jats:italic>-induction, predicate abstraction, and symbolic execution. We propose an augmented interpolation-based verification algorithm that injects external invariants into interpolation-based model checking<\/jats:italic> (McMillan, 2003<\/jats:ext-link>), a hardware model-checking algorithm recently adopted for software verification. The auxiliary invariants help prune unreachable states in Craig interpolants and confine the analysis to the reachable parts of a program. We implemented the proposed technique in the verification framework\u00a0CPAchecker<\/jats:sc> and evaluated it against mature SMT-based methods in\u00a0CPAchecker<\/jats:sc> as well as other state-of-the-art software verifiers. We found that injecting invariants reduces the number of interpolation queries needed to prove safety properties and improves the run-time efficiency. Consequently, the proposed invariant-injection approach verified difficult tasks that none of its plain version (i.e., without invariants), the invariant generator, or any compared tools could solve.<\/jats:p>","DOI":"10.1007\/978-3-031-66149-5_13","type":"book-chapter","created":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T07:01:54Z","timestamp":1728716514000},"page":"227-247","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Augmenting Interpolation-Based Model Checking with Auxiliary Invariants"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4832-7662","authenticated-orcid":false,"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5139-5178","authenticated-orcid":false,"given":"Po-Chun","family":"Chien","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8096-5595","authenticated-orcid":false,"given":"Nian-Ze","family":"Lee","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,10,13]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","unstructured":"Beyer, D., Chien, P.C., Lee, N.Z.: Augmenting interpolation-based model checking with auxiliary invariants (Extended version). arXiv\/CoRR 2403(07821) (March 2024). https:\/\/doi.org\/10.48550\/arXiv.2403.07821","DOI":"10.48550\/arXiv.2403.07821"},{"key":"13_CR2","unstructured":"Myers, G.J., Sandler, C., Badgett, T.: The Art of Software Testing. Wiley, 3rd edn. (2011). https:\/\/www.worldcat.org\/isbn\/978-1-119-20248-6"},{"key":"13_CR3","doi-asserted-by":"publisher","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Computing Surveys 41(4) (2009). https:\/\/doi.org\/10.1145\/1592434.1592438","DOI":"10.1145\/1592434.1592438"},{"key":"13_CR4","doi-asserted-by":"publisher","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: Proc. POPL. pp. 194\u2013206. ACM (1973). https:\/\/doi.org\/10.1145\/512927.512945","DOI":"10.1145\/512927.512945"},{"key":"13_CR5","doi-asserted-by":"publisher","unstructured":"Kam, J., Ullman, J.: Global data-flow analysis and iterative algorithms. J. ACM 23, 158\u2013171 (1976). https:\/\/doi.org\/10.1145\/321921.321938","DOI":"10.1145\/321921.321938"},{"key":"13_CR6","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data-flow analysis. In: Program Flow Analysis: Theory and Applications. pp. 189\u2013233. Prentice-Hall (1981). https:\/\/www.worldcat.org\/isbn\/978-0-137-29681-1"},{"key":"13_CR7","unstructured":"Kennedy, K.: A survey of data-flow analysis techniques. In: Program Flow Analysis: Theory and Applications, pp. 5\u201354. Prentice Hall (1981). https:\/\/www.worldcat.org\/isbn\/978-0-137-29681-1"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"Jones, N.D., Muchnick, S.S.: A flexible approach to interprocedural data-flow analysis and programs with recursive data structures. In: Proc. POPL. pp. 66\u201374. ACM (1982). https:\/\/doi.org\/10.1145\/582153.582161","DOI":"10.1145\/582153.582161"},{"key":"13_CR9","doi-asserted-by":"publisher","unstructured":"Ryder, B.G.: Incremental data-flow analysis. In: Proc. POPL. pp. 167\u2013176. ACM (1983). https:\/\/doi.org\/10.1145\/567067.567084","DOI":"10.1145\/567067.567084"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Reps, T.W., Horwitz, S., Sagiv, M.: Precise interprocedural data-flow analysis via graph reachability. In: Proc. POPL. pp. 49\u201361. ACM (1995). https:\/\/doi.org\/10.1145\/199448.199462","DOI":"10.1145\/199448.199462"},{"key":"13_CR11","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Proc. CAV. pp. 1\u201313. LNCS\u00a02725, Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"13_CR12","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":"13_CR13","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Proc. CAV. pp. 123\u2013136. LNCS\u00a04144, Springer (2006). https:\/\/doi.org\/10.1007\/11817963_14","DOI":"10.1007\/11817963_14"},{"key":"13_CR14","doi-asserted-by":"publisher","unstructured":"Vizel, Y., Grumberg, O.: Interpolation-sequence based model checking. In: Proc. FMCAD. pp.\u00a01\u20138. IEEE (2009). https:\/\/doi.org\/10.1109\/FMCAD.2009.5351148","DOI":"10.1109\/FMCAD.2009.5351148"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Lazy annotation for program testing and verification. In: Proc. CAV. pp. 104\u2013118. LNCS\u00a06174, Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_10","DOI":"10.1007\/978-3-642-14295-6_10"},{"key":"13_CR16","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A.: Software model checking via IC3. In: Proc. CAV. pp. 277\u2013293. LNCS\u00a07358, Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_23","DOI":"10.1007\/978-3-642-31424-7_23"},{"key":"13_CR17","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":"13_CR18","doi-asserted-by":"publisher","unstructured":"Awedh, M., Somenzi, F.: Automatic invariant strengthening to prove properties in bounded model checking. In: Proc. DAC. pp. 1073\u20131076. ACM (2006). https:\/\/doi.org\/10.1145\/1146909.1147180","DOI":"10.1145\/1146909.1147180"},{"key":"13_CR19","doi-asserted-by":"publisher","unstructured":"Ganai, M.K., Gupta, A.: Accelerating high-level bounded model checking. In: Proc. ICCAD. pp. 794\u2013801. ACM (2006). https:\/\/doi.org\/10.1145\/1233501.1233664","DOI":"10.1145\/1233501.1233664"},{"key":"13_CR20","doi-asserted-by":"publisher","unstructured":"Cheng, X., Hsiao, M.S.: Simulation-directed invariant mining for software verification. In: Proc. DATE. pp. 682\u2013687. ACM (2008). https:\/\/doi.org\/10.1109\/DATE.2008.4484757","DOI":"10.1109\/DATE.2008.4484757"},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"Donaldson, A.F., Haller, L., Kr\u00f6ning, D.: Strengthening induction-based race checking with lightweight static analysis. In: Proc. VMCAI. pp. 169\u2013183. LNCS\u00a06538, Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_13","DOI":"10.1007\/978-3-642-18275-4_13"},{"key":"13_CR22","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction with continuously-refined invariants. In: Proc. CAV. pp. 622\u2013640. LNCS\u00a09206, Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_42","DOI":"10.1007\/978-3-319-21690-4_42"},{"key":"13_CR23","doi-asserted-by":"publisher","unstructured":"Brain, M., Joshi, S., Kr\u00f6ning, D., Schrammel, P.: Safety verification and refutation by k-invariants and k-induction. In: Proc. SAS. pp. 145\u2013161. LNCS\u00a09291, Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-48288-9_9","DOI":"10.1007\/978-3-662-48288-9_9"},{"key":"13_CR24","doi-asserted-by":"publisher","unstructured":"Rocha, H., Ismail, H.I., Cordeiro, L.C., Barreto, R.S.: Model checking embedded C software using k-induction and invariants. In: Proc. SBESC. pp. 90\u201395. IEEE (2015). https:\/\/doi.org\/10.1109\/SBESC.2015.24","DOI":"10.1109\/SBESC.2015.24"},{"key":"13_CR25","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":"13_CR26","doi-asserted-by":"publisher","unstructured":"Fischer, J., Jhala, R., Majumdar, R.: Joining data flow with predicates. In: Proc. FSE. pp. 227\u2013236. ACM (2005). https:\/\/doi.org\/10.1145\/1081706.1081742","DOI":"10.1145\/1081706.1081742"},{"key":"13_CR27","doi-asserted-by":"publisher","unstructured":"Jain, H., Ivancic, F., Gupta, A., Shlyakhter, I., Wang, C.: Using statically computed invariants inside the predicate abstraction and refinement loop. In: Proc. CAV. pp. 137\u2013151. LNCS\u00a04144, Springer (2006). https:\/\/doi.org\/10.1007\/11817963_15","DOI":"10.1007\/11817963_15"},{"key":"13_CR28","doi-asserted-by":"publisher","unstructured":"Pasareanu, C.S., Visser, W.: Verification of Java programs using symbolic execution and invariant generation. In: Proc. SPIN. pp. 164\u2013181. LNCS\u00a02989, Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24732-6_13","DOI":"10.1007\/978-3-540-24732-6_13"},{"key":"13_CR29","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Proc. CAV. pp. 343\u2013361. LNCS\u00a09206, Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"13_CR30","unstructured":"Beyer, D., Lee, N.Z., Wendler, P.: Interpolation and SAT-based model checking revisited: Adoption to software verification. J. Autom. Reasoning (2024), accepted, preprint available via https:\/\/doi.org\/10.48550\/arXiv.2208.05046"},{"key":"13_CR31","doi-asserted-by":"publisher","unstructured":"Case, M.L., Mishchenko, A., Brayton, R.K.: Automated extraction of inductive invariants to aid model checking. In: Proc. FMCAD. pp. 165\u2013172 (2007). https:\/\/doi.org\/10.1109\/FAMCAD.2007.12","DOI":"10.1109\/FAMCAD.2007.12"},{"key":"13_CR32","doi-asserted-by":"publisher","unstructured":"Cabodi, G., Nocco, S., Quer, S.: Strengthening model checking techniques with inductive invariants. IEEE Trans. on CAD of Integrated Circuits and Systems 28(1), 154\u2013158 (2009). https:\/\/doi.org\/10.1109\/TCAD.2008.2009147","DOI":"10.1109\/TCAD.2008.2009147"},{"key":"13_CR33","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":"13_CR34","doi-asserted-by":"publisher","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Proc. CAV. pp. 184\u2013190. LNCS\u00a06806, Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"13_CR35","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Progress on software verification: SV-COMP 2022. In: Proc. TACAS\u00a0(2). pp. 375\u2013402. LNCS\u00a013244, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_20","DOI":"10.1007\/978-3-030-99527-0_20"},{"key":"13_CR36","doi-asserted-by":"publisher","unstructured":"Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Global value numbers and redundant computations. In: Proc. POPL. pp. 12\u201327. ACM (1988). https:\/\/doi.org\/10.1145\/73560.73562","DOI":"10.1145\/73560.73562"},{"key":"13_CR37","doi-asserted-by":"publisher","unstructured":"Bodik, R., Anik, S.: Path-sensitive value-flow analysis. In: Proc. POPL. pp. 237\u2013251. ACM (1998). https:\/\/doi.org\/10.1145\/268946.268966","DOI":"10.1145\/268946.268966"},{"key":"13_CR38","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proc. Int. Symp. on Programming. pp. 106\u2013130. Dunod (1976). https:\/\/www.di.ens.fr\/~cousot\/COUSOTpapers\/publications.www\/CousotCousot-ISOP-76-Dunod-p106--130-1976.pdf"},{"key":"13_CR39","doi-asserted-by":"publisher","unstructured":"Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation. Formal Asp. Comput. 20(4-5), 379\u2013405 (2008). https:\/\/doi.org\/10.1007\/s00165-008-0080-9","DOI":"10.1007\/s00165-008-0080-9"},{"key":"13_CR40","doi-asserted-by":"publisher","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Proc. VMCAI. pp. 70\u201387. LNCS\u00a06538, Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"13_CR41","doi-asserted-by":"publisher","unstructured":"Fedyukovich, G., Bod\u00edk, R.: Accelerating syntax-guided invariant synthesis. In: Proc. TACAS. pp. 251\u2013269. LNCS\u00a010805, Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_14","DOI":"10.1007\/978-3-319-89960-2_14"},{"key":"13_CR42","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). pp. 3\u201321. LNCS\u00a012078, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_1","DOI":"10.1007\/978-3-030-45190-5_1"},{"key":"13_CR43","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. pp. 55\u201362. EPTCS\u00a072, EPTCS (2011). https:\/\/doi.org\/10.4204\/EPTCS.72.6","DOI":"10.4204\/EPTCS.72.6"},{"key":"13_CR44","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, pp. 672\u2013678. LNCS\u00a07358, Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_48","DOI":"10.1007\/978-3-642-31424-7_48"},{"key":"13_CR45","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. pp. 846\u2013862. LNCS\u00a08044, Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_59","DOI":"10.1007\/978-3-642-39799-8_59"},{"key":"13_CR46","doi-asserted-by":"publisher","unstructured":"Brat, G., Navas, J.A., Shi, N., Venet, A.: Ikos: A framework for static analysis based on abstract interpretation. In: Proc. SEFM. pp. 271\u2013277. LNCS\u00a08702, Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-10431-7_20","DOI":"10.1007\/978-3-319-10431-7_20"},{"key":"13_CR47","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":"13_CR48","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. pp. 504\u2013518. LNCS\u00a04590, Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_51","DOI":"10.1007\/978-3-540-73368-3_51"},{"key":"13_CR49","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Proc. FMCAD. pp. 189\u2013197. FMCAD (2010). https:\/\/dl.acm.org\/doi\/10.5555\/1998496.1998532"},{"key":"13_CR50","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Wendler, P.: A unifying view on SMT-based software verification. J. Autom. Reasoning 60(3), 299\u2013335 (2018). https:\/\/doi.org\/10.1007\/s10817-017-9432-6","DOI":"10.1007\/s10817-017-9432-6"},{"key":"13_CR51","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":"13_CR52","doi-asserted-by":"publisher","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with Pvs. In: Proc. CAV. pp. 72\u201383. LNCS\u00a01254, Springer (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_10","DOI":"10.1007\/3-540-63166-6_10"},{"key":"13_CR53","doi-asserted-by":"publisher","unstructured":"Slab\u00fd, J., Strej\u010dek, J., Trt\u00edk, M.: Checking properties described by state machines: On synergy of instrumentation, slicing, and symbolic execution. In: Proc. FMICS. pp. 207\u2013221. LNCS\u00a07437, Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-32469-7_14","DOI":"10.1007\/978-3-642-32469-7_14"},{"key":"13_CR54","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley (1986). https:\/\/www.worldcat.org\/isbn\/978-0-201-10088-4"},{"key":"13_CR55","doi-asserted-by":"publisher","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","DOI":"10.1007\/s10703-011-0124-2"},{"key":"13_CR56","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: Requirements and solutions. Int. J. Softw. Tools Technol. Transfer 21(1), 1\u201329 (2019). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","DOI":"10.1007\/s10009-017-0469-y"},{"key":"13_CR57","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Proc. TACAS. pp. 93\u2013107. LNCS\u00a07795, Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"13_CR58","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Verifiers and validators of the 11th Intl. Competition on Software Verification (SV-COMP 2022). Zenodo (2022). https:\/\/doi.org\/10.5281\/zenodo.5959149","DOI":"10.5281\/zenodo.5959149"},{"key":"13_CR59","doi-asserted-by":"publisher","unstructured":"Beyer, D., Chien, P.C., Lee, N.Z.: Reproduction package for SPIN\u00a02024 submission \u2018Augmenting interpolation-based model checking with auxiliary invariants\u2019. Zenodo (2024). https:\/\/doi.org\/10.5281\/zenodo.10548594","DOI":"10.5281\/zenodo.10548594"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66149-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T07:07:27Z","timestamp":1728716847000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66149-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,13]]},"ISBN":["9783031661488","9783031661495"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66149-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,10,13]]},"assertion":[{"value":"13 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This project was funded in part by the Deutsche Forschungsgemeinschaft (DFG) \u2013 (ConVeY).","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Funding Statement"}},{"value":"SPIN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Model Checking Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"spin2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/spin-web.github.io\/SPIN2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}