{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:02:45Z","timestamp":1776304965849,"version":"3.50.1"},"reference-count":84,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2025,3,11]],"date-time":"2025-03-11T00:00:00Z","timestamp":1741651200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,3,11]],"date-time":"2025-03-11T00:00:00Z","timestamp":1741651200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","award":["378803395"],"award-info":[{"award-number":["378803395"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2025,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Software verifiers have different strengths and weaknesses, depending on the characteristics of the verification task. It is well-known that combinations of verifiers via portfolio- and selection-based approaches can help to combine their strengths. In this paper, we investigate (a) how to easily compose such combinations from <jats:italic>existing<\/jats:italic>, \u2018off-the-shelf\u2019 verifiers without changing them and (b) how much performance improvement each combination can yield, regarding the effectiveness (number of solved verification tasks) and efficiency (consumed resources). First, we contribute a method to systematically and conveniently construct verifier combinations from existing tools using <jats:sc>CoVeriTeam<\/jats:sc>. We consider sequential portfolios, parallel portfolios, and algorithm selections. Second, we perform a large experiment to show that combinations can improve the verification results <jats:italic>without<\/jats:italic> additional computational resources. Our benchmark set is the category <jats:italic>ReachSafety<\/jats:italic> as used in the 11th Competition on Software Verification (SV-COMP\u00a02022). This category contains 5\u00a0400 verification tasks, with diverse characteristics. The key novelty of this work in comparison to the conference version of the article is to introduce a validation step into the verifier combinations. By validating the output of the verifier, we can mitigate the adverse effect of unsound tools on the performance of portfolios, especially parallel portfolios, as observed in our previous experiments. We confirm that combinations employing a validation process are significantly more robust against the inclusion of unsound verifiers. Finally, all combinations are constructed from off-the-shelf verifiers, that is, we use the verification tools as published. The results of our work suggest that users of combinations of verification tools can achieve a significant improvement at a negligible cost, and more robustness by using combinations with validators.<\/jats:p>","DOI":"10.1007\/s10703-024-00449-y","type":"journal-article","created":{"date-parts":[[2025,3,11]],"date-time":"2025-03-11T12:25:47Z","timestamp":1741695947000},"page":"99-130","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Construction of verifier combinations from off-the-shelf components"],"prefix":"10.1007","volume":"66","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-0001-6078-4175","authenticated-orcid":false,"given":"Sudeep","family":"Kanav","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3730-3745","authenticated-orcid":false,"given":"Tobias","family":"Kleinert","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2906-6508","authenticated-orcid":false,"given":"Cedric","family":"Richter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,3,11]]},"reference":[{"key":"449_CR1","doi-asserted-by":"publisher","unstructured":"Beyer D, Podelski A (2022) Software model checking: 20 years and beyond. In: Principles of systems design. LNCS, vol\u00a013660. Springer, pp 554\u2013582. https:\/\/doi.org\/10.1007\/978-3-031-22337-2_27","DOI":"10.1007\/978-3-031-22337-2_27"},{"issue":"1","key":"449_CR2","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"CAR Hoare","year":"2003","unstructured":"Hoare CAR (2003) The verifying compiler: a grand challenge for computing research. J. ACM 50(1):63\u201369. https:\/\/doi.org\/10.1145\/602382.602403","journal-title":"J. ACM"},{"key":"449_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8","author":"EM Clarke","year":"2018","unstructured":"Clarke EM, Henzinger TA, Veith H, Bloem R (2018) Handbook of model checking. Springer, Berlin. https:\/\/doi.org\/10.1007\/978-3-319-10575-8","journal-title":"Springer, Berlin."},{"issue":"1145\/1592434","key":"449_CR4","first-page":"1592438","volume":"10","author":"R Jhala","year":"2009","unstructured":"Jhala R, Majumdar R (2009) Software model checking. ACM Comput Surv. doi 10(1145\/1592434):1592438","journal-title":"ACM Comput Surv. doi"},{"key":"449_CR5","doi-asserted-by":"publisher","unstructured":"Beyer D (2022) Progress on software verification: SV-COMP 2022. In: Proceedings of TACAS\u00a0(2), LNCS, vol\u00a013244. Springer, pp 375\u2013402. https:\/\/doi.org\/10.1007\/978-3-030-99527-0_20","DOI":"10.1007\/978-3-030-99527-0_20"},{"issue":"1","key":"449_CR6","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1109\/MIS.2014.3","volume":"29","author":"B Beckert","year":"2014","unstructured":"Beckert B, H\u00e4hnle R (2014) Reasoning and verification: state of the art and current trends. IEEE Intell Syst 29(1):20\u201329. https:\/\/doi.org\/10.1109\/MIS.2014.3","journal-title":"IEEE Intell Syst"},{"key":"449_CR7","doi-asserted-by":"publisher","unstructured":"Beyer D, Gulwani S, Schmidt D (2018) Combining model checking and data-flow analysis. In: Handbook of model checking. Springer, pp 493\u2013540. https:\/\/doi.org\/10.1007\/978-3-319-10575-8_16","DOI":"10.1007\/978-3-319-10575-8_16"},{"key":"449_CR8","doi-asserted-by":"publisher","unstructured":"Garavel H, ter Beek MH, van\u00a0de Pol J (2020) The 2020 expert survey on formal methods. In: Proceedings of FMICS. LNCS, vol\u00a012327. Springer, pp 3\u201369.https:\/\/doi.org\/10.1007\/978-3-030-58298-2_1","DOI":"10.1007\/978-3-030-58298-2_1"},{"key":"449_CR9","doi-asserted-by":"publisher","unstructured":"Ball T, Rajamani SK (2002) The Slam project: debugging system software via static analysis. In: Proceedings of POPL. ACM, pp 1\u20133.https:\/\/doi.org\/10.1145\/503272.503274","DOI":"10.1145\/503272.503274"},{"key":"449_CR10","doi-asserted-by":"publisher","unstructured":"Khoroshilov AV, Mutilin VS, Petrenko AK, Zakharov V (2009) Establishing Linux driver verification process. In: Proceedings of Ershov memorial conference. LNCS, vol\u00a05947. Springer, pp 165\u2013176. https:\/\/doi.org\/10.1007\/978-3-642-11486-1_14","DOI":"10.1007\/978-3-642-11486-1_14"},{"issue":"4","key":"449_CR11","doi-asserted-by":"publisher","first-page":"772","DOI":"10.1002\/spe.2949","volume":"51","author":"N Chong","year":"2021","unstructured":"Chong N, Cook B, Eidelman J, Kallas K, Khazem K, Monteiro FR, Schwartz-Narbonne D, Tasiran S, Tautschnig M, Tuttle MR (2021) Code-level model checking in the software development workflow at Amazon Web Services. Softw Pract Exp 51(4):772\u2013797. https:\/\/doi.org\/10.1002\/spe.2949","journal-title":"Softw Pract Exp"},{"key":"449_CR12","doi-asserted-by":"publisher","unstructured":"Calcagno C, Distefano D, Dubreil J, Gabi D, Hooimeijer P, Luca M, O\u2019Hearn PW, Papakonstantinou I, Purbrick J, Rodriguez D (2015) Moving fast with software verification. In: Proceedings of NFM. LNCS, vol\u00a09058. Springer, pp 3\u201311. https:\/\/doi.org\/10.1007\/978-3-319-17524-9_1","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"449_CR13","doi-asserted-by":"publisher","unstructured":"Beyer D, Keremoglu ME (2011) CPAchecker: a tool for configurable software verification. In: Proceedings of CAV. LNCS, vol\u00a06806. Springer, pp 184\u2013190.https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"449_CR14","doi-asserted-by":"publisher","unstructured":"Dangl M, L\u00f6we S, Wendler P (2015) CPAchecker with support for recursive programs and floating-point arithmetic (competition contribution). In: Proceedings of TACAS. LNCS, vol\u00a09035. Springer, pp 423\u2013425.https:\/\/doi.org\/10.1007\/978-3-662-46681-0_34","DOI":"10.1007\/978-3-662-46681-0_34"},{"key":"449_CR15","doi-asserted-by":"publisher","unstructured":"Gadelha MYR, Monteiro FR, Cordeiro LC, Nicole DA (2019) Esbmc v6.0: verifying C programs using k-induction and invariant inference (competition contribution). In: Proceedings of TACAS\u00a0(3). LNCS, vol\u00a011429. Springer, pp 209\u2013213.https:\/\/doi.org\/10.1007\/978-3-030-17502-3_15","DOI":"10.1007\/978-3-030-17502-3_15"},{"issue":"7","key":"449_CR16","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1126\/science.275.5296.51","volume":"275","author":"BA Huberman","year":"1997","unstructured":"Huberman BA, Lukose RM, Hogg T (1997) An economics approach to hard computational problems. Science 275(7):51\u201354. https:\/\/doi.org\/10.1126\/science.275.5296.51","journal-title":"Science"},{"key":"449_CR17","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0065-2458(08)60520-3","volume":"15","author":"JR Rice","year":"1976","unstructured":"Rice JR (1976) The algorithm selection problem. Adv Comput 15:65\u2013118. https:\/\/doi.org\/10.1016\/S0065-2458(08)60520-3","journal-title":"The algorithm selection problem. Adv Comput"},{"key":"449_CR18","doi-asserted-by":"publisher","unstructured":"Beyer D, Kanav S (2022) CoVeriTeam: on-demand composition of cooperative verification systems. In: Proceedings of TACAS. LNCS, vol\u00a013243. Springer, pp 561\u2013579. https:\/\/doi.org\/10.1007\/978-3-030-99524-9_31","DOI":"10.1007\/978-3-030-99524-9_31"},{"key":"449_CR19","unstructured":"Beyer D, Kanav S, Wachowitz H. Source-code repository of CoVeriTeam. https:\/\/gitlab.com\/sosy-lab\/software\/coveriteam. Accessed 09 Feb 2023"},{"key":"449_CR20","doi-asserted-by":"publisher","unstructured":"Beyer D, Kanav S, Wachowitz H (2023) CoVeriTeam service: verification as a service. In: Proceedings of ICSE, companion. IEEE, pp 21\u201325.https:\/\/doi.org\/10.1109\/ICSE-Companion58688.2023.00017","DOI":"10.1109\/ICSE-Companion58688.2023.00017"},{"key":"449_CR21","doi-asserted-by":"publisher","unstructured":"Beyer D, Kanav S, Richter C (2022) Construction of verifier combinations based on off-the-shelf verifiers. In: Proceedings of FASE. Springer, pp 49\u201370. https:\/\/doi.org\/10.1007\/978-3-030-99429-7_3","DOI":"10.1007\/978-3-030-99429-7_3"},{"key":"449_CR22","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7838348","author":"D Beyer","year":"2023","unstructured":"Beyer D, Kanav S, Kleinert T, Richter C (2023) Reproduction package for FMSD article \u2018Construction of verifier combinations from off-the-shelf components\u2019. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.7838348","journal-title":"Zenodo"},{"key":"449_CR23","doi-asserted-by":"publisher","unstructured":"Wendler P (2013) CPAchecker with sequential combination of explicit-state analysis and predicate analysis (competition contribution). In: Proceedings of TACAS. LNCS, vol\u00a07795. Springer, pp 613\u2013615. https:\/\/doi.org\/10.1007\/978-3-642-36742-7_45","DOI":"10.1007\/978-3-642-36742-7_45"},{"key":"449_CR24","doi-asserted-by":"publisher","unstructured":"Heizmann M, Chen YF, Dietsch D, Greitschus M, Hoenicke J, Li Y, Nutz A, Musa B, Schilling C, Schindler T, Podelski A (2018) Ultimate Automizer and the search for perfect interpolants (competition contribution). In: Proceedings of TACAS\u00a0(2). LNCS, vol\u00a010806. Springer, pp 447\u2013451. https:\/\/doi.org\/10.1007\/978-3-319-89963-3_30","DOI":"10.1007\/978-3-319-89963-3_30"},{"key":"449_CR25","doi-asserted-by":"publisher","unstructured":"Kotoun M, Peringer P, \u0160okov\u00e1 V, Vojnar T (2016) Optimized PredatorHP and the SV-COMP heap and memory safety benchmark (competition contribution). In: Proceedings of TACAS. LNCS, vol\u00a09636. Springer, pp 942\u2013945.https:\/\/doi.org\/10.1007\/978-3-662-49674-9_66","DOI":"10.1007\/978-3-662-49674-9_66"},{"key":"449_CR26","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-319-49052-6_13","volume":"10028","author":"L Hol\u00edk","year":"2016","unstructured":"Hol\u00edk L, Kotoun M, Peringer P, \u0160okov\u00e1 V, Trt\u00edk M, Vojnar T (2016) Predator shape analysis tool suite. Proceedings of HVC. LNCS 10028:202\u2013209. https:\/\/doi.org\/10.1007\/978-3-319-49052-6_13","journal-title":"Proceedings of HVC. LNCS"},{"issue":"1","key":"449_CR27","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/s10515-020-00270-x","volume":"27","author":"C Richter","year":"2020","unstructured":"Richter C, H\u00fcllermeier E, Jakobs MC, Wehrheim H (2020) Algorithm selection for software validation based on graph kernels. Autom Softw Eng 27(1):153\u2013186. https:\/\/doi.org\/10.1007\/s10515-020-00270-x","journal-title":"Autom Softw Eng"},{"key":"449_CR28","doi-asserted-by":"publisher","unstructured":"Richter C, Wehrheim H (2020) Attend and represent: a novel view on algorithm selection for software verification. In: Proceedings of ASE, pp 1016\u20131028. https:\/\/doi.org\/10.1145\/3324884.3416633","DOI":"10.1145\/3324884.3416633"},{"key":"449_CR29","doi-asserted-by":"publisher","unstructured":"Beyer D, Dangl M (2018) Strategy selection for software verification based on boolean features: a simple but effective approach. In: Proceedings of ISoLA. LNCS, vol\u00a011245. Springer, pp 144\u2013159. https:\/\/doi.org\/10.1007\/978-3-030-03421-4_11","DOI":"10.1007\/978-3-030-03421-4_11"},{"key":"449_CR30","doi-asserted-by":"publisher","unstructured":"Demyanova Y, Pani T, Veith H, Zuleger F (2017) Empirical software metrics for benchmarking of veri- fication tools. Formal Methods Syst Des 50(2\u20133):289\u2013316. https:\/\/doi.org\/10.1007\/s10703-016-0264-5","DOI":"10.1007\/s10703-016-0264-5"},{"key":"449_CR31","doi-asserted-by":"publisher","unstructured":"Beyer D, Dangl M, Dietsch D, Heizmann M, Lemberger T, Tautschnig M (2022) Verification witnesses. ACM Trans Softw Eng Methodol 31(4):57:1-57:69. https:\/\/doi.org\/10.1145\/3477579","DOI":"10.1145\/3477579"},{"key":"449_CR32","doi-asserted-by":"publisher","unstructured":"Beyer D, Dangl M, Dietsch D, Heizmann M, Stahlbauer A (2015) Witness validation and stepwise testification across software verifiers. In: Proceedings of FSE. ACM, pp 721\u2013733. https:\/\/doi.org\/10.1145\/2786805.2786867","DOI":"10.1145\/2786805.2786867"},{"key":"449_CR33","doi-asserted-by":"publisher","unstructured":"Beyer D, Dangl M, Dietsch D, Heizmann M (2016) Correctness witnesses: exchanging verification results between verifiers. In: Proceedings of FSE. ACM, pp 326\u2013337. https:\/\/doi.org\/10.1145\/2950290.2950351","DOI":"10.1145\/2950290.2950351"},{"key":"449_CR34","doi-asserted-by":"publisher","unstructured":"Beyer D, Dangl M, Lemberger T, Tautschnig M (2018) Tests from witnesses: execution-based validation of verification results. In: Proceedings of TAP. LNCS, vol\u00a010889. Springer, pp 3\u201323. https:\/\/doi.org\/10.1007\/978-3-319-92994-1_1","DOI":"10.1007\/978-3-319-92994-1_1"},{"key":"449_CR35","doi-asserted-by":"publisher","unstructured":"Beyer D, Dangl M (2016) Verification-aided debugging: an interactive web-service for exploring error witnesses. In: Proceedings of CAV\u00a0(2). LNCS, vol\u00a09780. Springer, pp 502\u2013509.https:\/\/doi.org\/10.1007\/978-3-319-41540-6_28","DOI":"10.1007\/978-3-319-41540-6_28"},{"key":"449_CR36","doi-asserted-by":"publisher","unstructured":"Beyer D (2015) Software verification and verifiable witnesses (Report on SV-COMP 2015). In: Proceed- ings of TACAS. LNCS, vol\u00a09035. Springer, pp 401\u2013416.https:\/\/doi.org\/10.1007\/978-3-662-46681-0_31","DOI":"10.1007\/978-3-662-46681-0_31"},{"issue":"1","key":"449_CR37","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 (2019) Reliable benchmarking: requirements and solutions. Int J Softw Tools Technol Transf 21(1):1\u201329. https:\/\/doi.org\/10.1007\/s10009-017-0469-y","journal-title":"Int J Softw Tools Technol Transf"},{"key":"449_CR38","unstructured":"Kleinert T (2022) Developing a verifier based on parallel portfolio with CoVeriTeam. Bachelor\u2019s Thesis, LMU Munich, Software Systems Lab"},{"key":"449_CR39","doi-asserted-by":"publisher","unstructured":"Demyanova Y, Veith H, Zuleger F (2013) On the concept of variable roles and its use in software analysis. In: Proceedings of FMCAD. IEEE, pp 226\u2013230. https:\/\/doi.org\/10.1109\/FMCAD.2013.6679414","DOI":"10.1109\/FMCAD.2013.6679414"},{"key":"449_CR40","doi-asserted-by":"publisher","unstructured":"Apel S, Beyer D, Friedberger K, Raimondi F, Rhein A (2013) Domain types: abstract-domain selection based on variable usage. In: Proceedings of HVC. LNCS, vol\u00a08244. Springer, pp 262\u2013278. https:\/\/doi.org\/10.1007\/978-3-319-03077-7","DOI":"10.1007\/978-3-319-03077-7"},{"key":"449_CR41","doi-asserted-by":"publisher","unstructured":"Xu L, Hoos HH, Leyton-Brown K (2007) Hierarchical hardness models for SAT. In: International conference on principles and practice of constraint programming. Springer, pp 696\u2013711. https:\/\/doi.org\/10.1007\/978-3-540-74970-7_49","DOI":"10.1007\/978-3-540-74970-7_49"},{"key":"449_CR42","doi-asserted-by":"publisher","unstructured":"Kadioglu S, Malitsky Y, Sabharwal A, Samulowitz H, Sellmann M (2011) Algorithm selection and scheduling. In: Proceedings of CP. Springer, pp 454\u2013469.https:\/\/doi.org\/10.1007\/978-3-642-23786-7_35","DOI":"10.1007\/978-3-642-23786-7_35"},{"key":"449_CR43","doi-asserted-by":"publisher","unstructured":"Torgo L, Gama J (1996) Regression by classification. In: Brazilian symposium on artificial intelligence. Springer, pp 51\u201360.https:\/\/doi.org\/10.1007\/3-540-61859-7_6","DOI":"10.1007\/3-540-61859-7_6"},{"key":"449_CR44","doi-asserted-by":"publisher","unstructured":"Chalupa M, \u0158echt\u00e1\u010dkov\u00e1 A, Mihalkovi\u010d V, Zaoral L, Strej\u010dek J (2022) Symbiotic\u00a09: string analysis and backward symbolic execution with loop folding (competition contribution). In: Proceedings of TACAS\u00a0(2). LNCS, vol\u00a013244. Springer, pp 462\u2013467.https:\/\/doi.org\/10.1007\/978-3-030-99527-0_32","DOI":"10.1007\/978-3-030-99527-0_32"},{"key":"449_CR45","doi-asserted-by":"publisher","unstructured":"Kr\u00f6ning D, Tautschnig M (2014) Cbmc: C bounded model checker (competition contribution). In: Proceed- ings of TACAS. LNCS, vol\u00a08413. Springer, pp 389\u2013391.https:\/\/doi.org\/10.1007\/978-3-642-54862-8_26","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"449_CR46","doi-asserted-by":"publisher","unstructured":"Chaudhary E, Joshi S (2019) Pinaka: symbolic execution meets incremental solving (competition contribution). In: Proceedings of TACAS\u00a0(3). LNCS, vol\u00a011429. Springer, pp 234\u2013238. https:\/\/doi.org\/10.1007\/978-3-030-17502-3_20","DOI":"10.1007\/978-3-030-17502-3_20"},{"key":"449_CR47","doi-asserted-by":"publisher","unstructured":"Dietsch D, Heizmann M, Nutz A, Sch\u00e4tzle C, Sch\u00fcssele F (2020) Ultimate Taipan with symbolic interpretation and fluid abstractions (competition contribution). In: Proceedings of TACAS\u00a0(2). LNCS, vol\u00a012079. Springer, pp 418\u2013422.https:\/\/doi.org\/10.1007\/978-3-030-45237-7_32","DOI":"10.1007\/978-3-030-45237-7_32"},{"key":"449_CR48","doi-asserted-by":"publisher","unstructured":"Mal\u00edk V, Schrammel P, Vojnar T (2020) 2ls: Heap analysis and memory safety (competition contribution). In: Proceedings of TACAS\u00a0(2). LNCS, vol\u00a012079. Springer, pp 368\u2013372. https:\/\/doi.org\/10.1007\/978-3-030-45237-7_22","DOI":"10.1007\/978-3-030-45237-7_22"},{"key":"449_CR49","doi-asserted-by":"publisher","unstructured":"Darke P, Agrawal S, Venkatesh R (2021) VeriAbs: a tool for scalable verification by abstraction (competition contribution). In: Proceedings of TACAS\u00a0(2). LNCS, vol\u00a012652. Springer, pp 458\u2013462.https:\/\/doi.org\/10.1007\/978-3-030-72013-1_32","DOI":"10.1007\/978-3-030-72013-1_32"},{"key":"449_CR50","doi-asserted-by":"publisher","unstructured":"Richter C, Wehrheim H (2019) PeSCo: predicting sequential combinations of verifiers (competition contribution). In: Proceedings of TACAS\u00a0(3). LNCS, vol\u00a011429. Springer, pp 229\u2013233.https:\/\/doi.org\/10.1007\/978-3-030-17502-3_19","DOI":"10.1007\/978-3-030-17502-3_19"},{"key":"449_CR51","doi-asserted-by":"publisher","unstructured":"Leeson W, Dwyer, M (2022) Graves-CPA: a graph-attention verifier selector (competition contribution). In: Proceedings of TACAS\u00a0(2). LNCS, vol\u00a013244. Springer, pp 440\u2013445. https:\/\/doi.org\/10.1007\/978-3-030-99527-0_28","DOI":"10.1007\/978-3-030-99527-0_28"},{"key":"449_CR52","doi-asserted-by":"publisher","unstructured":"Beyer D, Strej\u010dek J (2022) Case study on verification-witness validators: where we are and where we go. In: Proceedings of SAS. LNCS, vol\u00a013790. Springer, pp 160\u2013174. https:\/\/doi.org\/10.1007\/978-3-031-22308-2_8","DOI":"10.1007\/978-3-031-22308-2_8"},{"key":"449_CR53","doi-asserted-by":"publisher","unstructured":"Ayaziov\u00e1 P, Chalupa M, Strej\u010dek J (2022) Symbiotic-Witch: a Klee-based violation witness checker (competition contribution). In: Proceedings of TACAS\u00a0(2). LNCS, vol\u00a013244. Springer, pp 468\u2013473.https:\/\/doi.org\/10.1007\/978-3-030-99527-0_33","DOI":"10.1007\/978-3-030-99527-0_33"},{"key":"449_CR54","doi-asserted-by":"publisher","unstructured":"\u0160vejda J, Berger P, Katoen JP (2020) Interpretation-based violation witness validation for C: NitWit. In: Proceedings of TACAS. LNCS, vol\u00a012078. Springer, pp 40\u201357. https:\/\/doi.org\/10.1007\/978-3-030-45190-5_3","DOI":"10.1007\/978-3-030-45190-5_3"},{"key":"449_CR55","doi-asserted-by":"publisher","unstructured":"Beyer D, Spiessl M (2020) MetaVal: witness validation via verification. In: Proceedings of CAV. LNCS, vol\u00a012225. Springer, pp 165\u2013177.https:\/\/doi.org\/10.1007\/978-3-030-53291-8_10","DOI":"10.1007\/978-3-030-53291-8_10"},{"key":"449_CR56","unstructured":"Collection of verification tasks. https:\/\/gitlab.com\/sosy-lab\/benchmarking\/sv-benchmarks. Accessed 01 Apr 2023"},{"key":"449_CR57","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5831003","author":"D Beyer","year":"2022","unstructured":"Beyer D (2022) SV-benchmarks: benchmark set for software verification and testing (SV-COMP 2022 and Test-Comp 2022). Zenodo. https:\/\/doi.org\/10.5281\/zenodo.5831003","journal-title":"Zenodo"},{"key":"449_CR58","doi-asserted-by":"publisher","unstructured":"Beyer D (2013) Second competition on software verification (Summary of SV-COMP 2013). In: Proceed- ings of TACAS. LNCS, vol\u00a07795. Springer, pp 594\u2013609. https:\/\/doi.org\/10.1007\/978-3-642-36742-7_43","DOI":"10.1007\/978-3-642-36742-7_43"},{"key":"449_CR59","doi-asserted-by":"publisher","unstructured":"Beyer D (2012) Competition on software verification (SV-COMP). In: Proceedings of TACAS. LNCS, vol\u00a07214. Springer, pp 504\u2013524.https:\/\/doi.org\/10.1007\/978-3-642-28756-5_38","DOI":"10.1007\/978-3-642-28756-5_38"},{"key":"449_CR60","doi-asserted-by":"publisher","unstructured":"Leino KRM (2010) Dafny: an automatic program verifier for functional correctness. In: Proceedings of LPAR. LNCS, vol\u00a06355. Springer, pp 348\u2013370.https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"449_CR61","doi-asserted-by":"publisher","unstructured":"Cuoq P, Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B (2012) Frama-C. In: Proceedings of SEFM. Springer, pp 233\u2013247.https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"449_CR62","doi-asserted-by":"publisher","unstructured":"Ahrendt W, Baar T, Beckert B, Bubel R, Giese M, H\u00e4hnle R, Menzel W, Mostowski W, Roth A, Schlager S, Schmitt PH (2005) The key tool. Softw Syst Model 4(1):32\u201354. https:\/\/doi.org\/10.1007\/s10270-004-0058-x","DOI":"10.1007\/s10270-004-0058-x"},{"key":"449_CR63","doi-asserted-by":"publisher","unstructured":"Blom S, Huisman M (2014) The VerCors tool for verification of concurrent programs. In: Proceedings of FM. LNCS, vol 8442. Springer, pp 127\u2013131. https:\/\/doi.org\/10.1007\/978-3-319-06410-9_9","DOI":"10.1007\/978-3-319-06410-9_9"},{"key":"449_CR64","doi-asserted-by":"publisher","unstructured":"Jacobs B, Smans J, Philippaerts P, Vogels F, Penninckx W, Piessens F (2011) VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Proceedings of NFM. LNCS, vol 6617. Springer, pp 41\u201355.https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"449_CR65","doi-asserted-by":"publisher","unstructured":"Peringer P, \u0160okov\u00e1 V, Vojnar T (2020) PredatorHP revamped (not only) for interval-sized memory regions and memory reallocation (competition contribution). In: Proceedings of TACAS\u00a0(2). LNCS, vol\u00a012079. Springer, pp 408\u2013412.https:\/\/doi.org\/10.1007\/978-3-030-45237-7_30","DOI":"10.1007\/978-3-030-45237-7_30"},{"key":"449_CR66","doi-asserted-by":"publisher","unstructured":"Albarghouthi A, Li Y, Gurfinkel A, Chechik M (2012) Ufo: a framework for abstraction- and interpolation-based software verification. In: Proceedings of CAV. LNCS, vol\u00a07358. Springer, pp 672\u2013678. https:\/\/doi.org\/10.1007\/978-3-642-31424-7_48","DOI":"10.1007\/978-3-642-31424-7_48"},{"key":"449_CR67","doi-asserted-by":"publisher","unstructured":"Beyer D, Wehrheim H (2020) Verification artifacts in cooperative verification: Survey and unifying component framework. In: Proceedings of ISoLA\u00a0(1). LNCS, vol\u00a012476. Springer, pp 143\u2013167.https:\/\/doi.org\/10.1007\/978-3-030-61362-4_8","DOI":"10.1007\/978-3-030-61362-4_8"},{"key":"449_CR68","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre JC, Paskevich A (2013) Why3: where programs meet provers. In: Programming languages and systems. Springer, pp 125\u2013128.https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"449_CR69","doi-asserted-by":"publisher","unstructured":"Beyer D, Henzinger TA, Keremoglu ME, Wendler P (2012) Conditional model checking: a technique to pass information between verifiers. In: Proceedings of FSE. ACM. https:\/\/doi.org\/10.1145\/2393596.2393664","DOI":"10.1145\/2393596.2393664"},{"key":"449_CR70","doi-asserted-by":"publisher","unstructured":"Beyer D, Jakobs MC, Lemberger T, Wehrheim H (2018) Reducer-based construction of conditional verifiers. In: Proceedings of ICSE. ACM, pp 1182\u20131193. https:\/\/doi.org\/10.1145\/3180155.3180259","DOI":"10.1145\/3180155.3180259"},{"key":"449_CR71","doi-asserted-by":"publisher","unstructured":"Beyer D, Jakobs MC (2020) Fred: conditional model checking via reducers and folders. In: Proceedings of SEFM. LNCS, vol\u00a012310. Springer, pp 113\u2013132. https:\/\/doi.org\/10.1007\/978-3-030-58768-0_7","DOI":"10.1007\/978-3-030-58768-0_7"},{"key":"449_CR72","doi-asserted-by":"publisher","unstructured":"Beyer D, Jakobs MC, Lemberger T (2020) Difference verification with conditions. In: Proceedings of SEFM. LNCS, vol\u00a012310. Springer, pp 133\u2013154.https:\/\/doi.org\/10.1007\/978-3-030-58768-0_8","DOI":"10.1007\/978-3-030-58768-0_8"},{"key":"449_CR73","doi-asserted-by":"publisher","unstructured":"Beyer D, Jakobs MC (2019) CoVeriTest: cooperative verifier-based testing. In: Proceedings of FASE. LNCS, vol\u00a011424. Springer, pp 389\u2013408.https:\/\/doi.org\/10.1007\/978-3-030-16722-6_23","DOI":"10.1007\/978-3-030-16722-6_23"},{"issue":"3","key":"449_CR74","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/s10009-020-00587-8","volume":"23","author":"D Beyer","year":"2021","unstructured":"Beyer D, Jakobs MC (2021) Cooperative verifier-based testing with CoVeriTest. Int J Softw Tools Technol Transf 23(3):313\u2013333. https:\/\/doi.org\/10.1007\/s10009-020-00587-8","journal-title":"Int J Softw Tools Technol Transf"},{"key":"449_CR75","unstructured":"Wotzlaw A, van\u00a0der Grinten A, Speckenmeyer E, Porschen S (2012) pfolioUZK: solver description. In: Proceedings of SAT challenge p\u00a045. https:\/\/helda.helsinki.fi\/handle\/10138\/34218"},{"key":"449_CR76","unstructured":"Roussel O (2011) Description of portfolio. In: Proceedings of SAT challenge, p\u00a046. https:\/\/helda.helsinki.fi\/handle\/10138\/34218"},{"key":"449_CR77","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1613\/jair.2490","volume":"32","author":"L Xu","year":"2008","unstructured":"Xu L, Hutter F, Hoos HH, Leyton-Brown K (2008) SATzilla: Portfolio-based algorithm selection for SAT. JAIR 32:565\u2013606. https:\/\/doi.org\/10.1613\/jair.2490","journal-title":"JAIR"},{"issue":"1\u20132","key":"449_CR78","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/BF00143877","volume":"1","author":"S Minton","year":"1996","unstructured":"Minton S (1996) Automatically configuring constraint satisfaction programs: a case study. Constraints 1(1\u20132):7\u201343. https:\/\/doi.org\/10.1007\/BF00143877","journal-title":"Constraints"},{"key":"449_CR79","unstructured":"Bordeaux L, Hamadi Y, Samulowitz H (2009) Experiments with massively parallel constraint solving. In: Proceedings of IJCAI. https:\/\/www.ijcai.org\/Proceedings\/09\/Papers\/081.pdf"},{"key":"449_CR80","doi-asserted-by":"publisher","unstructured":"Yun X, Epstein SL (2012) Learning algorithm portfolios for parallel execution. In: Proceedings of LION. Springer, pp 323\u2013338. https:\/\/doi.org\/10.1007\/978-3-642-34413-8_23","DOI":"10.1007\/978-3-642-34413-8_23"},{"key":"449_CR81","doi-asserted-by":"publisher","unstructured":"Kotthoff L (2016) Algorithm selection for combinatorial search problems: a survey. In: Data mining and constraint programming\u2014foundations of a cross-disciplinary approach. LNCS, vol\u00a010101. Springer, pp 149\u2013190.https:\/\/doi.org\/10.1007\/978-3-319-50137-6_7","DOI":"10.1007\/978-3-319-50137-6_7"},{"key":"449_CR82","doi-asserted-by":"publisher","unstructured":"Lindauer M, Hoos H, Hutter F (2015) From sequential algorithm selection to parallel portfolio selection. In: Proceedings of LION. Springer, pp 1\u201316.https:\/\/doi.org\/10.1007\/978-3-319-19084-6_1","DOI":"10.1007\/978-3-319-19084-6_1"},{"key":"449_CR83","unstructured":"Kashgarani H, Kotthoff L (2021) Is algorithm selection worth it? Comparing selecting single algorithms and parallel execution. In: AAAI workshop on meta-learning and MetaDL challenge. PMLR, pp 58\u201364. https:\/\/proceedings.mlr.press\/v140\/kashgarani21a.html"},{"key":"449_CR84","doi-asserted-by":"publisher","unstructured":"Beyer D (2024) State of the art in software verification and witness validation: SV-COMP 2024. In: Proceedings of TACAS\u00a0(3). LNCS, vol\u00a014572. Springer, pp 299\u2013329. https:\/\/doi.org\/10.1007\/978-3-031-57256-2_15","DOI":"10.1007\/978-3-031-57256-2_15"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00449-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-024-00449-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00449-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T10:01:21Z","timestamp":1748599281000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-024-00449-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,11]]},"references-count":84,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,5]]}},"alternative-id":["449"],"URL":"https:\/\/doi.org\/10.1007\/s10703-024-00449-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,3,11]]},"assertion":[{"value":"19 November 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 June 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 March 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}