{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:03:54Z","timestamp":1776373434484,"version":"3.51.2"},"reference-count":115,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2024,12,1]],"date-time":"2024-12-01T00:00:00Z","timestamp":1733011200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T00:00:00Z","timestamp":1736985600000},"content-version":"vor","delay-in-days":46,"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":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2024,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Six years ago, we performed the first large-scale comparison of automated test\u00a0generators and software model\u00a0checkers with respect to bug-finding capabilities on a benchmark set with 5693 C programs. Since then, the International Competition on Software Testing\u00a0(Test-Comp) has established standardized formats and community-agreed rules for the experimental comparison of test\u00a0generators. With this new context, it is time to revisit our initial question: Model\u00a0checkers or test\u00a0generators\u2014which tools are more effective in finding bugs in software? To answer this, we perform a comparative analysis on the tools and existing data published by two competitions, the International Competition on Software\u00a0Verification\u00a0(SV-COMP) and Test-Comp. The results provide two insights: (1)\u00a0Almost all test\u00a0generators that participate in Test-Comp use hybrid\u00a0approaches that include formal methods, and (2)\u00a0although the considered model\u00a0checkers are still highly competitive, they are now outperformed by the bug-finding capabilities of the considered test\u00a0generators.<\/jats:p>","DOI":"10.1007\/s10009-024-00769-8","type":"journal-article","created":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T09:26:31Z","timestamp":1737019591000},"page":"633-646","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Six years later: testing vs. model checking"],"prefix":"10.1007","volume":"26","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-0003-0291-815X","authenticated-orcid":false,"given":"Thomas","family":"Lemberger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,1,16]]},"reference":[{"key":"769_CR1","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/978-3-030-72013-1_27","volume-title":"Proc. TACAS (2)","author":"Z. \u00c1d\u00e1m","year":"2021","unstructured":"\u00c1d\u00e1m, Z., Sallai, G., Hajdu, \u00c1.: Gazer-Theta: LLVM-based verifier portfolio with BMC\/CEGAR (competition contribution). In: Proc. TACAS (2). LNCS, vol.\u00a012652, pp.\u00a0433\u2013437. Springer, Berlin (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_27"},{"key":"769_CR2","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/978-3-030-99527-0_34","volume-title":"Proc. TACAS (2)","author":"Z. \u00c1d\u00e1m","year":"2022","unstructured":"\u00c1d\u00e1m, Z., Bajczi, L., Dobos-Kov\u00e1cs, M., Hajdu, A., Moln\u00e1r, V.: Theta: portfolio of cegar-based analyses with dynamic algorithm selection (competition contribution). In: Proc. TACAS (2). LNCS, vol.\u00a013244, pp.\u00a0474\u2013478. Springer, Berlin (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_34"},{"key":"769_CR3","doi-asserted-by":"publisher","first-page":"1138","DOI":"10.1109\/ASE.2019.00121","volume-title":"Proc. ASE","author":"M. Afzal","year":"2019","unstructured":"Afzal, M., Asia, A., Chauhan, A., Chimdyalwar, B., Darke, P., Datar, A., Kumar, S., Venkatesh, R.: VeriAbs: verification by abstraction and test generation. In: Proc. ASE, pp.\u00a01138\u20131141. IEEE (2019). https:\/\/doi.org\/10.1109\/ASE.2019.00121"},{"key":"769_CR4","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-031-30826-0_18","volume-title":"Proc. FASE","author":"M. Aldughaim","year":"2023","unstructured":"Aldughaim, M., Alshmrany, K.M., Gadelha, M.R., de Freitas, R., Cordeiro, L.C.: FuSeBMC_IA: interval analysis and methods for test-case generation (competition contribution). In: Proc. FASE. LNCS, vol.\u00a013991, pp.\u00a0324\u2013329. Springer, Berlin (2023). https:\/\/doi.org\/10.1007\/978-3-031-30826-0_18"},{"key":"769_CR5","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-030-79379-1_6","volume-title":"Proc. TAP","author":"K.M. Alshmrany","year":"2021","unstructured":"Alshmrany, K.M., Aldughaim, M., Bhayat, A., Cordeiro, L.C.: FuSeBMC: an energy-efficient test generator for finding security vulnerabilities in C programs. In: Proc. TAP, pp.\u00a085\u2013105. Springer, Berlin (2021). https:\/\/doi.org\/10.1007\/978-3-030-79379-1_6"},{"key":"769_CR6","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-030-99429-7_19","volume-title":"Proc. FASE","author":"K. Alshmrany","year":"2022","unstructured":"Alshmrany, K., Aldughaim, M., Cordeiro, L., Bhayat, A.: FuSeBMC v. 4: smart seed generation for hybrid fuzzing (competition contribution). In: Proc. FASE. LNCS, vol.\u00a013241, pp.\u00a0336\u2013340. Springer, Berlin (2022). https:\/\/doi.org\/10.1007\/978-3-030-99429-7_19"},{"issue":"5","key":"769_CR7","doi-asserted-by":"publisher","first-page":"66:1","DOI":"10.1145\/3106739","volume":"50","author":"E. Andreasen","year":"2017","unstructured":"Andreasen, E., Gong, L., M\u00f8ller, A., Pradel, M., Selakovic, M., Sen, K., Staicu, C.: A survey of dynamic analysis and test generation for JavaScript. ACM Comput. Surv. 50(5), 66:1\u201366:36 (2017). https:\/\/doi.org\/10.1145\/3106739","journal-title":"ACM Comput. Surv."},{"key":"769_CR8","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-662-54580-5_22","volume-title":"Proc. TACAS","author":"P. Andrianov","year":"2017","unstructured":"Andrianov, P., Friedberger, K., Mandrykin, M.U., Mutilin, V.S., Volkov, A.: CPA-BAM-BnB: block-abstraction memoization and region-based memory models for predicate abstractions (competition contribution). In: Proc. TACAS. LNCS, vol.\u00a010206, pp.\u00a0355\u2013359. Springer, Berlin (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_22"},{"key":"769_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-66149-5_11","volume-title":"Proc. SPIN. LNCS","author":"P. Ayaziov\u00e1","year":"2024","unstructured":"Ayaziov\u00e1, P., Beyer, D., Lingsch-Rosenfeld, M., Spiessl, M., Strej\u010dek, J.: Software verification witnesses 2.0. In: Proc. SPIN. LNCS, vol.\u00a014624. Springer, Berlin (2024). https:\/\/doi.org\/10.1007\/978-3-031-66149-5_11"},{"issue":"3","key":"769_CR10","doi-asserted-by":"publisher","first-page":"50:1","DOI":"10.1145\/3182657","volume":"51","author":"R. Baldoni","year":"2018","unstructured":"Baldoni, R., Coppa, E., D\u2019Elia, D.C., Demetrescu, C., Finocchi, I.: A survey of symbolic-execution techniques. ACM Comput. Surv. 51(3), 50:1\u201350:39 (2018). https:\/\/doi.org\/10.1145\/3182657","journal-title":"ACM Comput. Surv."},{"key":"769_CR11","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-319-68167-2_14","volume-title":"Proc. ATVA","author":"Z. Baranov\u00e1","year":"2017","unstructured":"Baranov\u00e1, Z., Barnat, J., Kejstov\u00e1, K., Ku\u010dera, T., Lauko, H., Mr\u00e1zek, J., Ro\u010dkai, P., \u0160till, V.: Model checking of C and C++ with Divine 4. In: Proc. ATVA. LNCS, vol.\u00a010482, pp.\u00a0201\u2013207. Springer, Berlin (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_14"},{"key":"769_CR12","doi-asserted-by":"publisher","first-page":"727","DOI":"10.1007\/978-3-319-10575-8_22","volume-title":"Handbook of Model Checking","author":"D.A. Basin","year":"2018","unstructured":"Basin, D.A., Cremers, C., Meadows, C.A.: Model checking security protocols. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp.\u00a0727\u2013762. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_22"},{"issue":"1","key":"769_CR13","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.: Reasoning and verification: state of the art and current trends. IEEE Intell. Syst. 29(1), 20\u201329 (2014). https:\/\/doi.org\/10.1109\/MIS.2014.3","journal-title":"IEEE Intell. Syst."},{"key":"769_CR14","unstructured":"BenchExec: A framework for reliable benchmarking and resource measurement. https:\/\/github.com\/sosy-lab\/benchexec. Accessed: 2024\u201310\u201331"},{"key":"769_CR15","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-662-46681-0_31","volume-title":"Proc. TACAS","author":"D. Beyer","year":"2015","unstructured":"Beyer, D.: Software verification and verifiable witnesses (report on SV-COMP 2015). In: Proc. TACAS. LNCS, vol.\u00a09035, pp.\u00a0401\u2013416. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_31"},{"key":"769_CR16","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-031-30820-8_29","volume-title":"Proc. TACAS (2)","author":"D. Beyer","year":"2023","unstructured":"Beyer, D.: Competition on software verification and witness validation: SV-COMP 2023. In: Proc. TACAS (2). LNCS, vol.\u00a013994, pp.\u00a0495\u2013522. Springer, Berlin (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_29"},{"key":"769_CR17","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Results of the 12th Intl. Competition on Software Verification (SV-COMP 2023). Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.7627787","DOI":"10.5281\/zenodo.7627787"},{"key":"769_CR18","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Results of the 5th Intl. Competition on Software Testing (Test-Comp 2023). Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.7701122","DOI":"10.5281\/zenodo.7701122"},{"key":"769_CR19","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-031-30826-0_17","volume-title":"Proc. FASE","author":"D. Beyer","year":"2023","unstructured":"Beyer, D.: Software testing: 5th comparative evaluation: Test-Comp 2023. In: Proc. FASE. LNCS, vol.\u00a013991, pp.\u00a0309\u2013323. Springer, Berlin (2023). https:\/\/doi.org\/10.1007\/978-3-031-30826-0_17"},{"key":"769_CR20","doi-asserted-by":"publisher","unstructured":"Beyer, D.: SV-Benchmarks: Benchmark set for software verification and testing (SV-COMP 2023 and Test-Comp 2023). Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.7627783","DOI":"10.5281\/zenodo.7627783"},{"key":"769_CR21","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Test-suite generators and validator of the 5th Intl. Competition on Software Testing (Test-Comp 2023). Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.7701118","DOI":"10.5281\/zenodo.7701118"},{"key":"769_CR22","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Test suites from test-generation tools (Test-Comp 2023). Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.7701126","DOI":"10.5281\/zenodo.7701126"},{"key":"769_CR23","unstructured":"Beyer, D.: 12th Intl. Competition on Software Verification (SV-COMP 2023): Results of the Competition. https:\/\/sv-comp.sosy-lab.org\/2023\/results\/results-verified\/. Accessed: 2024\u201310\u201331"},{"key":"769_CR24","unstructured":"Beyer, D.: 12th Intl. Competition on Software Verification (SV-COMP 2023): Submission. https:\/\/sv-comp.sosy-lab.org\/2023\/submission.php. Accessed: 2024\u201310\u201331"},{"key":"769_CR25","unstructured":"Beyer, D.: 5th Intl. Competition on Software Testing (Test-Comp 2023): Results of the Competition. https:\/\/test-comp.sosy-lab.org\/2023\/results\/results-verified\/. Accessed: 2024\u201310\u201331"},{"key":"769_CR26","unstructured":"Beyer, D.: 5th Intl. Competition on Software Testing (Test-Comp 2023): Submission. https:\/\/test-comp.sosy-lab.org\/2023\/submission.php. Accessed: 2024\u201310\u201331"},{"key":"769_CR27","unstructured":"Beyer, D.: Intl. Competition on Software Testing (Test-Comp). https:\/\/test-comp.sosy-lab.org\/. Accessed: 2024\u201310\u201331"},{"key":"769_CR28","unstructured":"Beyer, D.: Intl. Competition on Software Verification (SV-COMP). https:\/\/sv-comp.sosy-lab.org\/. Accessed: 2024\u201310\u201431"},{"issue":"3","key":"769_CR29","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, M.C.: Cooperative verifier-based testing with CoVeriTest. Int. J. Softw. Tools Technol. Transf. 23(3), 313\u2013333 (2021). https:\/\/doi.org\/10.1007\/s10009-020-00587-8","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"769_CR30","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1007\/978-3-030-99524-9_31","volume-title":"Proc. TACAS","author":"D. Beyer","year":"2022","unstructured":"Beyer, D., Kanav, S.: CoVeriTeam: on-demand composition of cooperative verification systems. In: Proc. TACAS. LNCS, vol.\u00a013243, pp.\u00a0561\u2013579. Springer, Berlin (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_31"},{"key":"769_CR31","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Proc. CAV","author":"D. Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Proc. CAV. LNCS, vol.\u00a06806, pp.\u00a0184\u2013190. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"key":"769_CR32","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-319-70389-3_7","volume-title":"Proc. HVC","author":"D. Beyer","year":"2017","unstructured":"Beyer, D., Lemberger, T.: Software verification: testing vs. model checking. In: Proc. HVC. LNCS, vol.\u00a010629, pp.\u00a099\u2013114. Springer, Berlin (2017). https:\/\/doi.org\/10.1007\/978-3-319-70389-3_7"},{"key":"769_CR33","doi-asserted-by":"publisher","first-page":"1074","DOI":"10.1109\/ASE.2019.00105","volume-title":"Proc. ASE","author":"D. Beyer","year":"2019","unstructured":"Beyer, D., Lemberger, T.: TestCov: robust test-suite execution and coverage measurement. In: Proc. ASE, pp.\u00a01074\u20131077. IEEE (2019). https:\/\/doi.org\/10.1109\/ASE.2019.00105"},{"key":"769_CR34","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lemberger, T.: Reproduction Package for STTT Article \u201cSix Years Later: Testing vs. Model Checking\u201d. Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.10232648","DOI":"10.5281\/zenodo.10232648"},{"key":"769_CR35","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/978-3-030-99527-0_26","volume-title":"Proc. TACAS (2)","author":"D. Beyer","year":"2022","unstructured":"Beyer, D., Spiessl, M.: The static analyzer Frama-C in SV-COMP (competition contribution). In: Proc. TACAS (2). LNCS, vol.\u00a013244, pp.\u00a0429\u2013434. Springer, Berlin (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_26"},{"key":"769_CR36","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1109\/ICSE.2004.1317455","volume-title":"Proc. ICSE","author":"D. Beyer","year":"2004","unstructured":"Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating tests from counterexamples. In: Proc. ICSE, pp.\u00a0326\u2013335. IEEE (2004). https:\/\/doi.org\/10.1109\/ICSE.2004.1317455"},{"key":"769_CR37","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1145\/2786805.2786867","volume-title":"Proc. FSE","author":"D. Beyer","year":"2015","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Stahlbauer, A.: Witness validation and stepwise testification across software verifiers. In: Proc. FSE, pp.\u00a0721\u2013733. ACM, New York (2015). https:\/\/doi.org\/10.1145\/2786805.2786867"},{"key":"769_CR38","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1145\/2950290.2950351","volume-title":"Proc. FSE","author":"D. Beyer","year":"2016","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: exchanging verification results between verifiers. In: Proc. FSE, pp.\u00a0326\u2013337. ACM, New York (2016). https:\/\/doi.org\/10.1145\/2950290.2950351"},{"key":"769_CR39","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-92994-1_1","volume-title":"Proc. TAP","author":"D. Beyer","year":"2018","unstructured":"Beyer, D., Dangl, M., Lemberger, T., Tautschnig, M.: Tests from witnesses: execution-based validation of verification results. In: Proc. TAP. LNCS, vol.\u00a010889, pp.\u00a03\u201323. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-92994-1_1"},{"issue":"1","key":"769_CR40","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."},{"issue":"4","key":"769_CR41","doi-asserted-by":"publisher","first-page":"57:1","DOI":"10.1145\/3477579","volume":"31","author":"D. Beyer","year":"2022","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Lemberger, T., Tautschnig, M.: Verification witnesses. ACM Trans. Softw. Eng. Methodol. 31(4), 57:1\u201357:69 (2022). https:\/\/doi.org\/10.1145\/3477579","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"769_CR42","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-030-99429-7_3","volume-title":"Proc. FASE","author":"D. Beyer","year":"2022","unstructured":"Beyer, D., Kanav, S., Richter, C.: Construction of verifier combinations based on off-the-shelf verifiers. In: Proc. FASE, pp.\u00a049\u201370. Springer, Berlin (2022). https:\/\/doi.org\/10.1007\/978-3-030-99429-7_3"},{"key":"769_CR43","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Proc. TACAS","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proc. TACAS. LNCS, vol.\u00a01579, pp.\u00a0193\u2013207. Springer, Berlin (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"769_CR44","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-662-48288-9_9","volume-title":"Proc. SAS.","author":"M. Brain","year":"2015","unstructured":"Brain, M., Joshi, S., Kr\u00f6ning, D., Schrammel, P.: Safety verification and refutation by k-invariants and k-induction. In: Proc. SAS. LNCS, vol.\u00a09291, pp.\u00a0145\u2013161. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-662-48288-9_9"},{"key":"769_CR45","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/978-3-030-99527-0_22","volume-title":"Proc. TACAS (2)","author":"L. Bu","year":"2022","unstructured":"Bu, L., Xie, Z., Lyu, L., Li, Y., Guo, X., Zhao, J., Li, X.: Brick: path enumeration-based bounded reachability checking of C programs (competition contribution). In: Proc. TACAS (2). LNCS, vol.\u00a013244, pp.\u00a0408\u2013412. Springer, Berlin (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_22"},{"key":"769_CR46","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-662-46675-9_6","volume-title":"Proc. FASE","author":"J. B\u00fcrdek","year":"2015","unstructured":"B\u00fcrdek, J., Lochau, M., Bauregger, S., Holzer, A., von Rhein, A., Apel, S., Beyer, D.: Facilitating reuse in multi-goal test-suite generation for software product lines. In: Proc. FASE. LNCS, vol.\u00a09033, pp.\u00a084\u201399. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-662-46675-9_6"},{"issue":"6","key":"769_CR47","doi-asserted-by":"publisher","first-page":"867","DOI":"10.1007\/s10009-020-00570-3","volume":"23","author":"C. Cadar","year":"2021","unstructured":"Cadar, C., Nowack, M.: Klee symbolic execution engine in 2019 (competition contribution). Int. J. Softw. Tools Technol. Transf. 23(6), 867\u2013870 (2021). https:\/\/doi.org\/10.1007\/s10009-020-00570-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"2","key":"769_CR48","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/2408776.2408795","volume":"56","author":"C. Cadar","year":"2013","unstructured":"Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun. ACM 56(2), 82\u201390 (2013). https:\/\/doi.org\/10.1145\/2408776.2408795","journal-title":"Commun. ACM"},{"key":"769_CR49","first-page":"209","volume-title":"Proc. OSDI","author":"C. Cadar","year":"2008","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proc. OSDI, pp.\u00a0209\u2013224. USENIX Association (2008)"},{"key":"769_CR50","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-17524-9_1","volume-title":"Proc. NFM","author":"C. Calcagno","year":"2015","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, vol.\u00a09058, pp.\u00a03\u201311. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_1"},{"key":"769_CR51","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"535","DOI":"10.1007\/978-3-031-30820-8_32","volume-title":"Proc. TACAS (2)","author":"M. Chalupa","year":"2023","unstructured":"Chalupa, M., Henzinger, T.: Bubaak: runtime monitoring of program verifiers (competition contribution). In: Proc. TACAS (2). LNCS, vol.\u00a013994, pp.\u00a0535\u2013540. Springer, Berlin (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_32"},{"key":"769_CR52","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-319-94111-0_7","volume-title":"Proc. SPIN","author":"M. Chalupa","year":"2018","unstructured":"Chalupa, M., Strej\u010dek, J., Vitovsk\u00e1, M.: Joint forces for memory safety checking. In: Proc. SPIN, pp.\u00a0115\u2013132. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-94111-0_7"},{"key":"769_CR53","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-030-71500-7_20","volume-title":"Proc. FASE","author":"M. Chalupa","year":"2021","unstructured":"Chalupa, M., Nov\u00e1k, J., Strej\u010dek, J.: Symbiotic 8: parallel and targeted test generation (competition contribution). In: Proc. FASE. LNCS, vol.\u00a012649, pp.\u00a0368\u2013372. Springer, Berlin (2021). https:\/\/doi.org\/10.1007\/978-3-030-71500-7_20"},{"key":"769_CR54","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-030-99527-0_32","volume-title":"Proc. TACAS (2)","author":"M. Chalupa","year":"2022","unstructured":"Chalupa, M., \u0158echt\u00e1\u010dkov\u00e1, A., Mihalkovi\u010d, V., Zaoral, L., Strej\u010dek, J.: Symbiotic 9: string analysis and backward symbolic execution with loop folding (competition contribution). In: Proc. TACAS (2). LNCS, vol.\u00a013244, pp.\u00a0462\u2013467. Springer, Berlin (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_32"},{"key":"769_CR55","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/978-3-030-17502-3_20","volume-title":"Proc. TACAS (3)","author":"E. Chaudhary","year":"2019","unstructured":"Chaudhary, E., Joshi, S.: Pinaka: symbolic execution meets incremental solving (competition contribution). In: Proc. TACAS (3). LNCS, vol.\u00a011429, pp.\u00a0234\u2013238. Springer, Berlin (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_20"},{"key":"769_CR56","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-030-17502-3_22","volume-title":"Proc. TACAS (3)","author":"A.B. Chowdhury","year":"2019","unstructured":"Chowdhury, A.B., Medicherla, R.K., Venkatesh, R.: VeriFuzz: program-aware fuzzing (competition contribution). In: Proc. TACAS (3). LNCS, vol.\u00a011429, pp.\u00a0244\u2013249. Springer, Berlin (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_22"},{"key":"769_CR57","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Proc. TACAS","author":"E.M. Clarke","year":"2004","unstructured":"Clarke, E.M., Kr\u00f6ning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Proc. TACAS. LNCS, vol.\u00a02988, pp.\u00a0168\u2013176. Springer, Berlin (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"769_CR58","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Handbook of Model Checking","author":"E.M. Clarke","year":"2018","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R.: Handbook of Model Checking. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8"},{"issue":"6","key":"769_CR59","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"M.R. Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010). https:\/\/doi.org\/10.3233\/JCS-2009-0393","journal-title":"J. Comput. Secur."},{"key":"769_CR60","unstructured":"Collection of verification tasks. https:\/\/gitlab.com\/sosy-lab\/benchmarking\/sv-witnesses. Accessed: 2024\u201310\u201331"},{"key":"769_CR61","unstructured":"Collection of verification tasks. https:\/\/gitlab.com\/sosy-lab\/benchmarking\/sv-benchmarks. Accessed: 2024\u201310\u201331"},{"key":"769_CR62","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Proc. SEFM","author":"P. Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Proc. SEFM, pp.\u00a0233\u2013247. Springer, Berlin (2012). https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16"},{"key":"769_CR63","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-662-46681-0_34","volume-title":"Proc. TACAS","author":"M. Dangl","year":"2015","unstructured":"Dangl, M., L\u00f6we, S., Wendler, P.: CPAchecker with support for recursive programs and floating-point arithmetic (competition contribution). In: Proc. TACAS. LNCS, vol.\u00a09035, pp.\u00a0423\u2013425. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_34"},{"key":"769_CR64","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1007\/978-3-030-72013-1_32","volume-title":"Proc. TACAS (2)","author":"P. Darke","year":"2021","unstructured":"Darke, P., Agrawal, S., Venkatesh, R.: VeriAbs: a tool for scalable verification by abstraction (competition contribution). In: Proc. TACAS (2). LNCS, vol.\u00a012652, pp.\u00a0458\u2013462. Springer, Berlin (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_32"},{"key":"769_CR65","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"588","DOI":"10.1007\/978-3-031-30820-8_41","volume-title":"Proc. TACAS (2)","author":"P. Darke","year":"2023","unstructured":"Darke, P., Chimdyalwar, B., Agrawal, S., Venkatesh, R., Chakraborty, S., Kumar, S.: VeriAbsL: scalable verification by abstraction and strategy prediction (competition contribution). In: Proc. TACAS (2). LNCS, vol.\u00a013994, pp.\u00a0588\u2013593. Springer, Berlin (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_41"},{"key":"769_CR66","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/978-3-030-45237-7_32","volume-title":"Proc. TACAS (2)","author":"D. Dietsch","year":"2020","unstructured":"Dietsch, D., Heizmann, M., Nutz, A., Sch\u00e4tzle, C., Sch\u00fcssele, F.: Ultimate Taipan with symbolic interpretation and fluid abstractions (competition contribution). In: Proc. TACAS (2). LNCS, vol.\u00a012079, pp.\u00a0418\u2013422. Springer, Berlin (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_32"},{"key":"769_CR67","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/978-3-319-48869-1_5","volume-title":"Proc. VSTTE","author":"R. Dockins","year":"2016","unstructured":"Dockins, R., Foltzer, A., Hendrix, J., Huffman, B., McNamee, D., Tomb, A.: Constructing semantic models of programs with the software analysis workbench. In: Proc. VSTTE. LNCS, vol.\u00a09971, pp.\u00a056\u201372. Springer, Berlin (2016). https:\/\/doi.org\/10.1007\/978-3-319-48869-1_5"},{"issue":"7","key":"769_CR68","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","volume":"27","author":"V. D\u2019Silva","year":"2008","unstructured":"D\u2019Silva, V., Kr\u00f6ning, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 27(7), 1165\u20131178 (2008). https:\/\/doi.org\/10.1109\/TCAD.2008.923410","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"769_CR69","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/978-3-642-27940-9_13","volume-title":"Proc. VMCAI","author":"E. Ermis","year":"2012","unstructured":"Ermis, E., Hoenicke, J., Podelski, A.: Splitting via interpolants. In: Proc. VMCAI. LNCS, vol.\u00a07148, pp.\u00a0186\u2013201. Springer, Berlin (2012). https:\/\/doi.org\/10.1007\/978-3-642-27940-9_13"},{"key":"769_CR70","doi-asserted-by":"publisher","unstructured":"Ernst, G.: A complete approach to loop verification with invariants and summaries. Tech. Rep. (2020) https:\/\/doi.org\/10.48550\/arXiv.2010.05812. arXiv:2010.05812v2","DOI":"10.48550\/arXiv.2010.05812"},{"issue":"1","key":"769_CR71","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s10009-015-0407-9","volume":"19","author":"M.Y. Gadelha","year":"2017","unstructured":"Gadelha, M.Y., Ismail, H.I., Cordeiro, L.C.: Handling loops in bounded model checking of C programs via k-induction. Int. J. Softw. Tools Technol. Transf. 19(1), 97\u2013114 (2017). https:\/\/doi.org\/10.1007\/s10009-015-0407-9","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"769_CR72","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-030-17502-3_15","volume-title":"Proc. TACAS (3)","author":"M.Y.R. Gadelha","year":"2019","unstructured":"Gadelha, M.Y.R., Monteiro, F.R., Cordeiro, L.C., Nicole, D.A.: Esbmc v6.0: verifying C programs using k-induction and invariant inference (competition contribution). In: Proc. TACAS (3). LNCS, vol.\u00a011429, pp.\u00a0209\u2013213. Springer, Berlin (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_15"},{"key":"769_CR73","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-58298-2_1","volume-title":"Proc. FMICS","author":"H. Garavel","year":"2020","unstructured":"Garavel, H., ter Beek, M.H., van de Pol, J.: The 2020 expert survey on formal methods. In: Proc. FMICS. LNCS, vol.\u00a012327, pp.\u00a03\u201369. Springer, Berlin (2020). https:\/\/doi.org\/10.1007\/978-3-030-58298-2_1"},{"key":"769_CR74","unstructured":"GDart-LLVM. https:\/\/github.com\/tudo-aqua\/gdart-llvm. Accessed: 2024\u201310\u201331"},{"key":"769_CR75","volume-title":"Proc. NDSS","author":"P. Godefroid","year":"2008","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. In: Proc. NDSS (2008). The Internet Society. https:\/\/www.ndss-symposium.org\/ndss2008\/automated-whitebox-fuzz-testing\/"},{"key":"769_CR76","unstructured":"Graves-Parallel. https:\/\/github.com\/mgerrard\/graves-par. Accessed: 2024\u201310\u201331"},{"key":"769_CR77","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-319-66706-5_7","volume-title":"Proc. SAS","author":"M. Greitschus","year":"2017","unstructured":"Greitschus, M., Dietsch, D., Podelski, A.: Loop invariants from counterexamples. In: Proc. SAS. LNCS, vol.\u00a010422, pp.\u00a0128\u2013147. Springer, Berlin (2017). https:\/\/doi.org\/10.1007\/978-3-319-66706-5_7"},{"key":"769_CR78","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/978-3-319-10575-8_18","volume-title":"Handbook of Model Checking","author":"A. Gupta","year":"2018","unstructured":"Gupta, A., Kahlon, V., Qadeer, S., Touili, T.: Model checking concurrent programs. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp.\u00a0573\u2013611. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_18"},{"issue":"6","key":"769_CR79","doi-asserted-by":"publisher","first-page":"1051","DOI":"10.1007\/s10817-019-09535-x","volume":"64","author":"\u00c1. Hajdu","year":"2020","unstructured":"Hajdu, \u00c1., Micskei, Z.: Efficient strategies for CEGAR-based model checking. J. Autom. Reason. 64(6), 1051\u20131091 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09535-x","journal-title":"J. Autom. Reason."},{"key":"769_CR80","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-642-39799-8_2","volume-title":"Proc. CAV","author":"M. Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Proc. CAV. LNCS, vol.\u00a08044, pp.\u00a036\u201352. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_2"},{"key":"769_CR81","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-319-89963-3_30","volume-title":"Proc. TACAS (2)","author":"M. Heizmann","year":"2018","unstructured":"Heizmann, M., Chen, Y.F., Dietsch, D., Greitschus, M., Hoenicke, J., Li, Y., Nutz, A., Musa, B., Schilling, C., Schindler, T., Podelski, A.: Ultimate automizer and the search for perfect interpolants (competition contribution). In: Proc. TACAS (2). LNCS, vol.\u00a010806, pp.\u00a0447\u2013451. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_30"},{"key":"769_CR82","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-540-93900-9_15","volume-title":"Proc. VMCAI","author":"A. Holzer","year":"2009","unstructured":"Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: Query-driven program testing. In: Proc. VMCAI. LNCS, vol.\u00a05403, pp.\u00a0151\u2013166. Springer, Berlin (2009). https:\/\/doi.org\/10.1007\/978-3-540-93900-9_15"},{"key":"769_CR83","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1007\/978-3-642-31424-7_61","volume-title":"Proc. CAV","author":"J. Jaffar","year":"2012","unstructured":"Jaffar, J., Murali, V., Navas, J.A., Santosa, A.E.: TRACER: a symbolic execution tool for verification. In: Proc. CAV. LNCS, vol.\u00a07358, pp.\u00a0758\u2013766. Springer, Berlin (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_61"},{"key":"769_CR84","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/978-3-030-45234-6_28","volume-title":"Proc. FASE","author":"J. Jaffar","year":"2020","unstructured":"Jaffar, J., Maghareh, R., Godboley, S., Ha, X.L.: TracerX: dynamic symbolic execution with interpolation (competition contribution). In: Proc. FASE. LNCS, vol.\u00a012076, pp.\u00a0530\u2013534. Springer, Berlin (2020). https:\/\/doi.org\/10.1007\/978-3-030-45234-6_28"},{"key":"769_CR85","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-030-71500-7_18","volume-title":"Proc. FASE","author":"M.C. Jakobs","year":"2021","unstructured":"Jakobs, M.C., Richter, C.: CoVeriTest with adaptive time scheduling (competition contribution). In: Proc. FASE. LNCS, vol.\u00a012649, pp.\u00a0358\u2013362. Springer, Berlin (2021). https:\/\/doi.org\/10.1007\/978-3-030-71500-7_18"},{"issue":"4","key":"769_CR86","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R. Jhala","year":"2009","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 21 (2009). https:\/\/doi.org\/10.1145\/1592434.1592438","journal-title":"ACM Comput. Surv."},{"key":"769_CR87","series-title":"LNCS","first-page":"1","volume-title":"Proc. VSTTE","author":"M. Journault","year":"2019","unstructured":"Journault, M., Min\u00e9, A., Monat, R., Ouadjaout, A.: Combinations of reusable abstract domains for a multilingual static analyzer. In: Proc. VSTTE. LNCS, vol.\u00a012031, pp.\u00a01\u201318. Springer, Berlin (2019)"},{"key":"769_CR88","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-030-99527-0_30","volume-title":"Proc. TACAS (2)","author":"M. Kettl","year":"2022","unstructured":"Kettl, M., Lemberger, T.: The static analyzer Infer in SV-COMP (competition contribution). In: Proc. TACAS (2). LNCS, vol.\u00a013244, pp.\u00a0451\u2013456. Springer, Berlin (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_30"},{"key":"769_CR89","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Proc. TACAS","author":"D. Kr\u00f6ning","year":"2014","unstructured":"Kr\u00f6ning, D., Tautschnig, M.: Cbmc: C bounded model checker (competition contribution). In: Proc. TACAS. LNCS, vol.\u00a08413, pp.\u00a0389\u2013391. Springer, Berlin (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_26"},{"key":"769_CR90","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-030-02508-3_17","volume-title":"Proc. ICTAC","author":"H. Lauko","year":"2018","unstructured":"Lauko, H., Ro\u010dkai, P., Barnat, J.: Symbolic computation via program transformation. In: Proc. ICTAC. LNCS, vol.\u00a011187, pp.\u00a0313\u2013332. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-030-02508-3_17"},{"key":"769_CR91","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-030-99527-0_28","volume-title":"Proc. TACAS (2)","author":"W. Leeson","year":"2022","unstructured":"Leeson, W., Dwyer, M.: Graves-CPA: a graph-attention verifier selector (competition contribution). In: Proc. TACAS (2). LNCS, vol.\u00a013244, pp.\u00a0440\u2013445. Springer, Berlin (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_28"},{"key":"769_CR92","unstructured":"Legion\/SymCC. https:\/\/github.com\/gernst\/legion-symcc. Accessed: 2024\u201310\u201331"},{"issue":"6","key":"769_CR93","doi-asserted-by":"publisher","first-page":"871","DOI":"10.1007\/s10009-020-00568-x","volume":"23","author":"T. Lemberger","year":"2021","unstructured":"Lemberger, T.: Plain random test generation with PRTest (competition contribution). Int. J. Softw. Tools Technol. Transf. 23(6), 871\u2013873 (2021). https:\/\/doi.org\/10.1007\/s10009-020-00568-x","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"769_CR94","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/978-3-030-45234-6_31","volume-title":"Proc. FASE","author":"D. Liu","year":"2020","unstructured":"Liu, D., Ernst, G., Murray, T., Rubinstein, B.: Legion: best-first concolic testing (competition contribution). In: Proc. FASE. LNCS, vol.\u00a012076, pp.\u00a0545\u2013549. Springer, Berlin (2020). https:\/\/doi.org\/10.1007\/978-3-030-45234-6_31"},{"key":"769_CR95","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1145\/3324884.3416629","volume-title":"Proc. ASE","author":"D. Liu","year":"2020","unstructured":"Liu, D., Ernst, G., Murray, T., Rubinstein, B.I.P.: Legion: best-first concolic testing. In: Proc. ASE, pp.\u00a054\u201365. IEEE (2020). https:\/\/doi.org\/10.1145\/3324884.3416629"},{"key":"769_CR96","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-030-45237-7_22","volume-title":"Proc. TACAS (2)","author":"V. Mal\u00edk","year":"2020","unstructured":"Mal\u00edk, V., Schrammel, P., Vojnar, T.: 2ls: heap analysis and memory safety (competition contribution). In: Proc. TACAS (2). LNCS, vol.\u00a012079, pp.\u00a0368\u2013372. Springer, Berlin (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_22"},{"issue":"11","key":"769_CR97","doi-asserted-by":"publisher","first-page":"2312","DOI":"10.1109\/TSE.2019.2946563","volume":"47","author":"V.J.M. Man\u00e8s","year":"2021","unstructured":"Man\u00e8s, V.J.M., Han, H., Han, C., Cha, S.K., Egele, M., Schwartz, E.J., Woo, M.: The art, science, and engineering of fuzzing: a survey. IEEE Trans. Softw. Eng. 47(11), 2312\u20132331 (2021). https:\/\/doi.org\/10.1109\/TSE.2019.2946563","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"769_CR98","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1002\/stvr.294","volume":"14","author":"P. McMinn","year":"2004","unstructured":"McMinn, P.: Search-based software test-data generation: a survey. Softw. Test. Verif. Reliab. 14(2), 105\u2013156 (2004). https:\/\/doi.org\/10.1002\/stvr.294","journal-title":"Softw. Test. Verif. Reliab."},{"key":"769_CR99","doi-asserted-by":"publisher","first-page":"1419","DOI":"10.23919\/DATE54114.2022.9774672","volume-title":"Proc. DATE","author":"R. Metta","year":"2022","unstructured":"Metta, R., Medicherla, R.K., Chakraborty, S.: BMC+Fuzz: efficient and effective test generation. In: Proc. DATE, pp.\u00a01419\u20131424. IEEE (2022). https:\/\/doi.org\/10.23919\/DATE54114.2022.9774672"},{"key":"769_CR100","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-030-99429-7_20","volume-title":"Proc. FASE","author":"R. Metta","year":"2022","unstructured":"Metta, R., Medicherla, R.K., Karmarkar, H.: VeriFuzz: fuzz centric test generation tool (competition contribution). In: Proc. FASE. LNCS, vol.\u00a013241, pp.\u00a0341\u2013346. Springer, Berlin (2022). https:\/\/doi.org\/10.1007\/978-3-030-99429-7_20"},{"key":"769_CR101","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1007\/978-3-031-30820-8_37","volume-title":"Proc. TACAS (2)","author":"R. Monat","year":"2023","unstructured":"Monat, R., Ouadjaout, A., Min\u00e9, A.: Mopsa-C: modular domains and relational abstract interpretation for C programs (competition contribution). In: Proc. TACAS (2). LNCS, vol.\u00a013994, pp.\u00a0565\u2013570. Springer, Berlin (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_37"},{"key":"769_CR102","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1007\/978-3-662-46681-0_44","volume-title":"Proc. TACAS","author":"A. Nutz","year":"2015","unstructured":"Nutz, A., Dietsch, D., Mohamed, M.M., Podelski, A.: Ultimate Kojak with memory safety checks (competition contribution). In: Proc. TACAS. LNCS, vol.\u00a09035, pp.\u00a0458\u2013460. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_44"},{"key":"769_CR103","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/bs.adcom.2018.03.015","volume":"112","author":"M. Papadakis","year":"2019","unstructured":"Papadakis, M., Kintis, M., Zhang, J., Jia, Y., Traon, Y.L., Harman, M.: Chapter six\u00a0- mutation testing advances: an analysis and survey. Adv. Comput. 112, 275\u2013378 (2019). https:\/\/doi.org\/10.1016\/bs.adcom.2018.03.015","journal-title":"Adv. Comput."},{"issue":"4","key":"769_CR104","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/s10009-009-0118-1","volume":"11","author":"C.S. Pasareanu","year":"2009","unstructured":"Pasareanu, C.S., Visser, W.: A survey of new trends in symbolic execution for software testing and analysis. Int. J. Softw. Tools Technol. Transf. 11(4), 339\u2013353 (2009). https:\/\/doi.org\/10.1007\/s10009-009-0118-1","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"769_CR105","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-030-17502-3_19","volume-title":"Proc. TACAS (3)","author":"C. Richter","year":"2019","unstructured":"Richter, C., Wehrheim, H.: PeSCo: predicting sequential combinations of verifiers (competition contribution). In: Proc. TACAS (3). LNCS, vol.\u00a011429, pp.\u00a0229\u2013233. Springer, Berlin (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_19"},{"issue":"1","key":"769_CR106","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, M.C., Wehrheim, H.: Algorithm selection for software validation based on graph kernels. Autom. Softw. Eng. 27(1), 153\u2013186 (2020). https:\/\/doi.org\/10.1007\/s10515-020-00270-x","journal-title":"Autom. Softw. Eng."},{"key":"769_CR107","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"520","DOI":"10.1007\/978-3-030-45234-6_26","volume-title":"Proc. FASE","author":"S. Ruland","year":"2020","unstructured":"Ruland, S., Lochau, M., Jakobs, M.C.: HybridTiger: hybrid model checking and domination-based partitioning for efficient multi-goal test-suite generation (competition contribution). In: Proc. FASE. LNCS, vol.\u00a012076, pp.\u00a0520\u2013524. Springer, Berlin (2020). https:\/\/doi.org\/10.1007\/978-3-030-45234-6_26"},{"key":"769_CR108","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/978-3-030-72013-1_28","volume-title":"Proc. TACAS (2)","author":"S. Saan","year":"2021","unstructured":"Saan, S., Schwarz, M., Apinis, K., Erhard, J., Seidl, H., Vogler, R., Vojdani, V.: Goblint: thread-modular abstract interpretation using side-effecting constraints (competition contribution). In: Proc. TACAS (2). LNCS, vol.\u00a012652, pp.\u00a0438\u2013442. Springer, Berlin (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_28"},{"key":"769_CR109","doi-asserted-by":"publisher","unstructured":"Scott, R., Dockins, R., Ravitch, T., Tomb, A.: Crux: Symbolic execution meets SMT-based verification (competition contribution). Zenodo (2022). https:\/\/doi.org\/10.5281\/zenodo.6147218","DOI":"10.5281\/zenodo.6147218"},{"key":"769_CR110","unstructured":"Test-comp 2023 benchmarks test tasks. https:\/\/test-comp.sosy-lab.org\/2023\/benchmarks.php. Accessed: 2024\u201310\u201331"},{"key":"769_CR111","doi-asserted-by":"publisher","first-page":"176","DOI":"10.23919\/FMCAD.2017.8102257","volume-title":"Proc. FMCAD","author":"T. T\u00f3th","year":"2017","unstructured":"T\u00f3th, T., Hajdu, A., V\u00f6r\u00f6s, A., Micskei, Z., Majzik, I.: Theta: a framework for abstraction refinement-based model checking. In: Proc. FMCAD, pp.\u00a0176\u2013179 (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102257"},{"key":"769_CR112","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/1007512.1007526","volume-title":"Proc. ISSTA","author":"W. Visser","year":"2004","unstructured":"Visser, W., P\u0103s\u0103reanu, C.S., Khurshid, S.: Test-input generation with Java PathFinder. In: Proc. ISSTA, pp.\u00a097\u2013107. ACM, New York (2004). https:\/\/doi.org\/10.1145\/1007512.1007526"},{"key":"769_CR113","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/2970276.2970337","volume-title":"Proc. ASE","author":"V. Vojdani","year":"2016","unstructured":"Vojdani, V., Apinis, K., R\u00f5tov, V., Seidl, H., Vene, V., Vogler, R.: Static race detection for device drivers: the Goblint approach. In: Proc. ASE, pp.\u00a0391\u2013402. ACM, New York (2016). https:\/\/doi.org\/10.1145\/2970276.2970337"},{"key":"769_CR114","doi-asserted-by":"publisher","first-page":"203","DOI":"10.15514\/ISPRAS-2017-29(4)-13","volume":"29","author":"A.R. Volkov","year":"2017","unstructured":"Volkov, A.R., Mandrykin, M.U.: Predicate abstractions memory modeling method with separation into disjoint regions. Proc. Inst. Syst. Program. 29, 203\u2013216 (2017). https:\/\/doi.org\/10.15514\/ISPRAS-2017-29(4)-13","journal-title":"Proc. Inst. Syst. Program."},{"key":"769_CR115","unstructured":"wasp. https:\/\/github.com\/wasp-platform\/wasp. Accessed: 2024\u201310\u201331"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-024-00769-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-024-00769-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-024-00769-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,6]],"date-time":"2025-02-06T11:43:18Z","timestamp":1738842198000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-024-00769-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12]]},"references-count":115,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2024,12]]}},"alternative-id":["769"],"URL":"https:\/\/doi.org\/10.1007\/s10009-024-00769-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,12]]},"assertion":[{"value":"7 November 2024","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 January 2025","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}