{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T06:30:12Z","timestamp":1750746612551,"version":"3.37.3"},"reference-count":86,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2024,3,19]],"date-time":"2024-03-19T00:00:00Z","timestamp":1710806400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,3,19]],"date-time":"2024-03-19T00:00:00Z","timestamp":1710806400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100019559","name":"Carl von Ossietzky Universit\u00e4t Oldenburg","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100019559","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2024,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Cooperative software validation aims at having verification and\/or testing tools <jats:italic>cooperate<\/jats:italic> on the task of correctness checking. Cooperation involves the exchange of information about currently achieved results in the form of (verification) artifacts. These artifacts are typically specialized to the type of analysis performed by the tool, e.g.,\u00a0bounded model checking, abstract interpretation or symbolic execution, and hence require the definition of a new artifact for every new cooperation to be built. In this article, we introduce a unified artifact (called Generalized Information Exchange Automaton, short GIA) supporting the cooperation of <jats:italic>over-approximating<\/jats:italic> with <jats:italic>under-approximating<\/jats:italic> analyses. It provides information gathered by an analysis to its partner in a cooperation, independent of the type of analysis and usage context within software validation. We provide a formal definition of this artifact in the form of an automaton together with two operators on GIAs. The first operation <jats:italic>reduces<\/jats:italic> a program by excluding these parts, where the information that they are already processed is encoded in the GIA. The second operation combines partial results from two GIAs into a single on. We show that computed analysis results are never lost when connecting tools via these operations. To experimentally demonstrate the feasibility, we have implemented two such cooperation: one for verification and one for testing. The obtained results show the feasibility of our novel artifact in different contexts of cooperative software validation, in particular how the new artifact is able to overcome some drawbacks of existing artifacts.<\/jats:p>","DOI":"10.1007\/s10270-024-01155-3","type":"journal-article","created":{"date-parts":[[2024,3,19]],"date-time":"2024-03-19T08:02:17Z","timestamp":1710835337000},"page":"695-719","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Exchanging information in cooperative software validation"],"prefix":"10.1007","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5098-0495","authenticated-orcid":false,"given":"Jan","family":"Haltermann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,3,19]]},"reference":[{"key":"1155_CR1","doi-asserted-by":"publisher","unstructured":"\u00c1d\u00e1m, Z., Sallai, G., Hajdu, \u00c1.: Gazer-theta: Llvm-based verifier portfolio with BMC\/CEGAR (competition contribution). In: Groote, J.F., Larsen, K.G. (eds.) Proceedings TACAS. LNCS, vol. 12652, pp. 433\u2013437. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_27","DOI":"10.1007\/978-3-030-72013-1_27"},{"key":"1155_CR2","doi-asserted-by":"publisher","unstructured":"Albarghouthi, A., Gurfinkel, A., Chechik, M.: From under-approximations to over-approximations and back. In: Flanagan, C., K\u00f6nig, B. (eds.) Proceedings of the TACAS. LNCS, vol.\u00a07214, pp. 157\u2013172. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_12","DOI":"10.1007\/978-3-642-28756-5_12"},{"key":"1155_CR3","doi-asserted-by":"publisher","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: Proceedings of the TAP. LNCS, vol. 12740, pp. 85\u2013105. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-79379-1_6","DOI":"10.1007\/978-3-030-79379-1_6"},{"key":"1155_CR4","doi-asserted-by":"publisher","unstructured":"Avgerinos, T., Rebert, A., Cha, S.K., Brumley, D.: Enhancing symbolic execution with veritesting. In: Proceedings of the ICSE, pp. 1083\u20131094. ACM (2014). https:\/\/doi.org\/10.1145\/2568225.2568293","DOI":"10.1145\/2568225.2568293"},{"key":"1155_CR5","doi-asserted-by":"publisher","unstructured":"Beckman, N.E., Nori, A.V., Rajamani, S.K., Simmons, R.J.: Proofs from tests. In: Ryder, B.G., Zeller, A. (eds.) Proceedings of the ISSTA, pp. 3\u201314. ACM (2008). https:\/\/doi.org\/10.1145\/1390630.1390634","DOI":"10.1145\/1390630.1390634"},{"key":"1155_CR6","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M.: Strategy selection for software verification based on Boolean features: a simple but effective approach. In: Proceedings of the ISoLA. LNCS, vol. 11245, pp. 144\u2013159. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_11","DOI":"10.1007\/978-3-030-03421-4_11"},{"key":"1155_CR7","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lemberger, T.: Conditional testing: off-the-shelf combination of test-case generators. In: Proceedings of the ATVA. LNCS, vol. 11781, pp. 189\u2013208. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_11","DOI":"10.1007\/978-3-030-31784-3_11"},{"key":"1155_CR8","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Advances in automatic software testing: test-comp 2022. In: Johnsen, E.B., Wimmer, M. (eds.) Proceedings of the FASE. LNCS, vol. 13241, pp. 321\u2013335. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99429-7_18","DOI":"10.1007\/978-3-030-99429-7_18"},{"key":"1155_CR9","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Progress on software verification: SV-COMP 2022. In: Fisman, D., Rosu, G. (eds.) Proceedings of the TACAS. LNCS, vol. 13244, pp. 375\u2013402. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_20","DOI":"10.1007\/978-3-030-99527-0_20"},{"key":"1155_CR10","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: exchanging verification results between verifiers. In: Zimmermann, T., Cleland-Huang, J., Su, Z. (eds.) Proceedings of the FSE, pp. 326\u2013337. ACM (2016). https:\/\/doi.org\/10.1145\/2950290.2950351","DOI":"10.1145\/2950290.2950351"},{"issue":"4","key":"1155_CR11","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-57:69 (2022). https:\/\/doi.org\/10.1145\/3477579","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"1155_CR12","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Stahlbauer, A.: Witness validation and stepwise testification across software verifiers. In: Nitto, E.D., Harman, M., Heymans, P. (eds.) Proceedings of the ESEC\/FSE, pp. 721\u2013733. ACM (2015). https:\/\/doi.org\/10.1145\/2786805.2786867","DOI":"10.1145\/2786805.2786867"},{"key":"1155_CR13","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/978-3-319-10575-8_16","volume-title":"Handbook of Model Checking","author":"D Beyer","year":"2018","unstructured":"Beyer, D., Gulwani, S., Schmidt, D.A.: Combining model checking and data-flow analysis. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 493\u2013540. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_16"},{"issue":"5\u20136","key":"1155_CR14","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. Int. J. Softw. Tools Technol. Transf. 9(5\u20136), 505\u2013525 (2007). https:\/\/doi.org\/10.1007\/s10009-007-0044-z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1155_CR15","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Keremoglu, M.E., Wendler, P.: Conditional model checking: a technique to pass information between verifiers. In: Tracz, W., Robillard, M.P., Bultan, T. (eds.) Proceedings of the FSE, p.\u00a057. ACM (2012). https:\/\/doi.org\/10.1145\/2393596.2393664","DOI":"10.1145\/2393596.2393664"},{"key":"1155_CR16","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jakobs, M.: CoVeriTest: cooperative verifier-based testing. In: H\u00e4hnle, R., van\u00a0der Aalst, W.M.P. (eds.) Proceedings of the FASE. LNCS, vol. 11424, pp. 389\u2013408. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-16722-6_23","DOI":"10.1007\/978-3-030-16722-6_23"},{"key":"1155_CR17","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jakobs, M.: Fred: Conditional model checking via reducers and folders. In: de\u00a0Boer, F.S., Cerone, A. (eds.) Proceedings of the SEFM. LNCS, vol. 12310, pp. 113\u2013132. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-58768-0_7","DOI":"10.1007\/978-3-030-58768-0_7"},{"key":"1155_CR18","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jakobs, M., Lemberger, T., Wehrheim, H.: Reducer-based construction of conditional verifiers. In: Chaudron, M., Crnkovic, I., Chechik, M., Harman, M. (eds.) Proceedings of the ICSE, pp. 1182\u20131193. ACM (2018). https:\/\/doi.org\/10.1145\/3180155.3180259","DOI":"10.1145\/3180155.3180259"},{"key":"1155_CR19","doi-asserted-by":"publisher","unstructured":"Beyer, D., Kanav, S.: CoVeriTeam: on-demand composition of cooperative verification systems. In: Fisman, D., Rosu, G. (eds.) Proceedings of the TACAS. LNCS, vol. 13243, pp. 561\u2013579. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_31","DOI":"10.1007\/978-3-030-99524-9_31"},{"key":"1155_CR20","doi-asserted-by":"publisher","unstructured":"Beyer, D., Kanav, S., Richter, C.: Construction of verifier combinations based on off-the-shelf verifiers. In: Johnsen, E.B., Wimmer, M. (eds.) Proceedings of the FASE. LNCS, vol. 13241, pp. 49\u201370. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99429-7_3","DOI":"10.1007\/978-3-030-99429-7_3"},{"key":"1155_CR21","doi-asserted-by":"publisher","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) Proceedings of the CAV. LNCS, vol.\u00a06806, pp. 184\u2013190. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"1155_CR22","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lemberger, T.: Software verification: testing vs. model checking\u2014a comparative evaluation of the state of the art. In: Strichman, O., Tzoref-Brill, R. (eds.) Proceedings of the HVC. LNCS, vol. 10629, pp. 99\u2013114. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-70389-3_7","DOI":"10.1007\/978-3-319-70389-3_7"},{"key":"1155_CR23","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lemberger, T.: Testcov: robust test-suite execution and coverage measurement. In: Proceedings of the ASE, pp. 1074\u20131077. IEEE (2019). https:\/\/doi.org\/10.1109\/ASE.2019.00105","DOI":"10.1109\/ASE.2019.00105"},{"key":"1155_CR24","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lemberger, T., Haltermann, J., Wehrheim, H.: Decomposing software verification into off-the-shelf components: an application to CEGAR. In: Proceedings of the ICSE, pp. 536\u2013548. ACM (2022). https:\/\/doi.org\/10.1145\/3510003.3510064","DOI":"10.1145\/3510003.3510064"},{"issue":"1","key":"1155_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-017-0469-y","volume":"21","author":"D Beyer","year":"2019","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: requirements and solutions. Int. J. Softw. Tools Technol. Transf. 21(1), 1\u201329 (2019). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1155_CR26","doi-asserted-by":"publisher","unstructured":"Beyer, D., Wehrheim, H.: Verification artifacts in cooperative verification: survey and unifying component framework. In: Margaria, T., Steffen, B. (eds.) Proceedings of the ISoLA. LNCS, vol. 12476, pp. 143\u2013167. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_8","DOI":"10.1007\/978-3-030-61362-4_8"},{"key":"1155_CR27","doi-asserted-by":"publisher","unstructured":"Blicha, M., Hyv\u00e4rinen, A.E.J., Marescotti, M., Sharygina, N.: A cooperative parallelization approach for property-directed k-induction. In: Beyer, D., Zufferey, D. (eds.) Proceedings of the VMCAI. LNCS, vol. 11990, pp. 270\u2013292. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-39322-9_13","DOI":"10.1007\/978-3-030-39322-9_13"},{"key":"1155_CR28","doi-asserted-by":"publisher","unstructured":"Braione, P., Denaro, G., Mattavelli, A., Pezz\u00e8, M.: Combining symbolic execution and search-based testing for programs with complex heap inputs. In: Bultan, T., Sen, K. (eds.) Proceedings of the ISSTA, pp. 90\u2013101. ACM (2017). https:\/\/doi.org\/10.1145\/3092703.3092715","DOI":"10.1145\/3092703.3092715"},{"key":"1155_CR29","doi-asserted-by":"publisher","unstructured":"Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Halbwachs, N., Peled, D.A. (eds.) Proceedings of the CAV. LNCS, vol.\u00a01633, pp. 274\u2013287. Springer (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_25","DOI":"10.1007\/3-540-48683-6_25"},{"key":"1155_CR30","doi-asserted-by":"publisher","unstructured":"Bu, L., Xie, Z., Lyu, L., Li, Y., Guo, X., Zhao, J., Li, X.: BRICK: path enumeration based bounded reachability checking of C program (competition contribution). In: Fisman, D., Rosu, G. (eds.) Proceedings of the TACAS. LNCS, vol. 13244, pp. 408\u2013412. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_22","DOI":"10.1007\/978-3-030-99527-0_22"},{"key":"1155_CR31","doi-asserted-by":"publisher","unstructured":"Burnim, J., Sen, K.: Heuristics for scalable dynamic test generation. In: Proceedings of the ASE, pp. 443\u2013446. IEEE Computer Society (2008). https:\/\/doi.org\/10.1109\/ASE.2008.69","DOI":"10.1109\/ASE.2008.69"},{"key":"1155_CR32","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Draves, R., van Renesse, R. (eds.) Proceedings of the OSDI, pp. 209\u2013224. USENIX Association (2008)"},{"key":"1155_CR33","doi-asserted-by":"publisher","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Collaborative verification and testing with explicit assumptions. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) Proceedings of the FM. LNCS, vol.\u00a07436, pp. 132\u2013146. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_13","DOI":"10.1007\/978-3-642-32759-9_13"},{"key":"1155_CR34","doi-asserted-by":"publisher","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Guiding dynamic symbolic execution toward unverified program executions. In: Dillon, L.K., Visser, W., Williams, L. (eds.) Proceedings of the ICSE, pp. 144\u2013155. ACM (2016). https:\/\/doi.org\/10.1145\/2884781.2884843","DOI":"10.1145\/2884781.2884843"},{"key":"1155_CR35","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Proceedings of the CAV, pp. 154\u2013169. LNCS\u00a01855, Springer (2000). https:\/\/doi.org\/10.1007\/10722167_15","DOI":"10.1007\/10722167_15"},{"volume-title":"Handbook of Model Checking","year":"2018","key":"1155_CR36","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Berlin (2018)"},{"key":"1155_CR37","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Proceedings of the POPL, pp. 238\u2013252. ACM (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"1155_CR38","doi-asserted-by":"publisher","unstructured":"Csallner, C., Smaragdakis, Y.: Check \u2019n\u2019 Crash: combining static checking and testing. In: Roman, G., Griswold, W.G., Nuseibeh, B. (eds.) Proceedings of the ICSE, pp. 422\u2013431. ACM (2005). https:\/\/doi.org\/10.1145\/1062455.1062533","DOI":"10.1145\/1062455.1062533"},{"issue":"2","key":"1155_CR39","doi-asserted-by":"publisher","first-page":"8:1","DOI":"10.1145\/1348250.1348254","volume":"17","author":"C Csallner","year":"2008","unstructured":"Csallner, C., Smaragdakis, Y., Xie, T.: DSD-Crasher: a hybrid analysis tool for bug finding. TOSEM 17(2), 8:1-8:37 (2008). https:\/\/doi.org\/10.1145\/1348250.1348254","journal-title":"TOSEM"},{"key":"1155_CR40","doi-asserted-by":"publisher","unstructured":"Czech, M., H\u00fcllermeier, E., Jakobs, M., Wehrheim, H.: Predicting rankings of software verification tools. In: Proceedings of the SWAN, pp. 23\u201326. ACM (2017). https:\/\/doi.org\/10.1145\/3121257.3121262","DOI":"10.1145\/3121257.3121262"},{"key":"1155_CR41","doi-asserted-by":"publisher","unstructured":"Czech, M., Jakobs, M., Wehrheim, H.: Just test what you cannot verify! In: Egyed, A., Schaefer, I. (eds.) Proceedings of the FASE. LNCS, vol.\u00a09033, pp. 100\u2013114. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46675-9_7","DOI":"10.1007\/978-3-662-46675-9_7"},{"key":"1155_CR42","doi-asserted-by":"publisher","unstructured":"Daca, P., Gupta, A., Henzinger, T.A.: Abstraction-driven concolic testing. In: Jobstmann, B., Leino, K.R.M. (eds.) Proceedings of the VMCAI. LNCS, vol.\u00a09583, pp. 328\u2013347. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_16","DOI":"10.1007\/978-3-662-49122-5_16"},{"key":"1155_CR43","doi-asserted-by":"publisher","unstructured":"Dangl, M., L\u00f6we, S., Wendler, P.: CPAchecker with support for recursive programs and floating-point arithmetic-(competition contribution). In: Proceedings of the TACS. LNCS, vol.\u00a09035, pp. 423\u2013425. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_34","DOI":"10.1007\/978-3-662-46681-0_34"},{"key":"1155_CR44","doi-asserted-by":"publisher","unstructured":"Demyanova, Y., Pani, T., Veith, H., Zuleger, F.: Empirical software metrics for benchmarking of verification tools. In: Proceedings of the CAV. LNCS, vol.\u00a09206, pp. 561\u2013579. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_39","DOI":"10.1007\/978-3-319-21690-4_39"},{"key":"1155_CR45","doi-asserted-by":"publisher","unstructured":"Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) VSL. LNCS, vol.\u00a08559, pp. 737\u2013744. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"1155_CR46","doi-asserted-by":"publisher","unstructured":"Gao, M., He, L., Majumdar, R., Wang, Z.: LLSPLAT: improving concolic testing by bounded model checking. In: Proceedings of the SCAM, pp. 127\u2013136. IEEE (2016). https:\/\/doi.org\/10.1109\/SCAM.2016.26","DOI":"10.1109\/SCAM.2016.26"},{"key":"1155_CR47","doi-asserted-by":"publisher","unstructured":"Gargantini, A., Vavassori, P.: Using decision trees to aid algorithm selection in combinatorial interaction tests generation. In: Proceedings of the ICST, pp. 1\u201310. IEEE (2015). https:\/\/doi.org\/10.1109\/ICSTW.2015.7107442","DOI":"10.1109\/ICSTW.2015.7107442"},{"key":"1155_CR48","doi-asserted-by":"publisher","unstructured":"Ge, X., Taneja, K., Xie, T., Tillmann, N.: DyTa: dynamic symbolic execution guided with static verification results. In: Taylor, R.N., Gall, H.C., Medvidovic, N. (eds.) Proceedings of the ICSE, pp. 992\u2013994. ACM (2011). https:\/\/doi.org\/10.1145\/1985793.1985971","DOI":"10.1145\/1985793.1985971"},{"key":"1155_CR49","doi-asserted-by":"publisher","unstructured":"Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.: Compositional may-must program analysis: unleashing the power of alternation. In: Hermenegildo, M.V., Palsberg, J. (eds.) Proceedings of the POPL, pp. 43\u201356. ACM (2010). https:\/\/doi.org\/10.1145\/1706299.1706307","DOI":"10.1145\/1706299.1706307"},{"key":"1155_CR50","doi-asserted-by":"publisher","unstructured":"Groce, A., Zhang, C., Eide, E., Chen, Y., Regehr, J.: Swarm testing. In: Proceedings of the ISSTA, pp. 78\u201388. ACM (2012). https:\/\/doi.org\/10.1145\/2338965.2336763","DOI":"10.1145\/2338965.2336763"},{"key":"1155_CR51","doi-asserted-by":"publisher","unstructured":"Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: SYNERGY: a new algorithm for property checking. In: Young, M., Devanbu, P.T. (eds.) Proceedings of the FSE, pp. 117\u2013127. ACM (2006). https:\/\/doi.org\/10.1145\/1181775.1181790","DOI":"10.1145\/1181775.1181790"},{"key":"1155_CR52","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Ivrii, A.: K-induction without unrolling. In: Stewart, D., Weissenbacher, G. (eds.) Proceedings of the FMCAD, pp. 148\u2013155. IEEE (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102253","DOI":"10.23919\/FMCAD.2017.8102253"},{"key":"1155_CR53","doi-asserted-by":"publisher","unstructured":"Haltermann, J., Jakobs, M., Richter, C., Wehrheim, H.: Parallel program analysis via range splitting. In: Lambers, L., Uchitel, S. (eds.) Proceedings of the FASE. LNCS, vol. 13991, pp. 195\u2013219. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30826-0_11","DOI":"10.1007\/978-3-031-30826-0_11"},{"key":"1155_CR54","doi-asserted-by":"publisher","unstructured":"Haltermann, J., Jakobs, M., Richter, C., Wehrheim, H.: Ranged program analysis via instrumentation. In: Ferreira, C., Willemse, T.A.C. (eds.) Proceedings of the SEFM. LNCS, vol. 14323, pp. 145\u2013164. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-47115-5_9","DOI":"10.1007\/978-3-031-47115-5_9"},{"key":"1155_CR55","doi-asserted-by":"publisher","unstructured":"Haltermann, J., Wehrheim, H.: CoVEGI: cooperative verification via externally generated invariants. In: Guerra, E., Stoelinga, M. (eds.) Proceedings of the FASE. LNCS, vol. 12649, pp. 108\u2013129. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-71500-7_6","DOI":"10.1007\/978-3-030-71500-7_6"},{"key":"1155_CR56","doi-asserted-by":"publisher","unstructured":"Haltermann, J., Wehrheim, H.: Information exchange between over- and underapproximating software analyses. In: Schlingloff, B., Chai, M. (eds.) Proceedings of the SEFM. LNCS, vol. 13550, pp. 37\u201354. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-17108-6_3","DOI":"10.1007\/978-3-031-17108-6_3"},{"key":"1155_CR57","doi-asserted-by":"publisher","unstructured":"Haltermann, J., Wehrheim, H.: Artifact for \u2019information exchange between over- and underapproximating software analyses (2023). https:\/\/doi.org\/10.5281\/zenodo.6749669","DOI":"10.5281\/zenodo.6749669"},{"key":"1155_CR58","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Chen, Y., 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: Proceedings of the TACAS. LNCS, vol. 10806, pp. 447\u2013451. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_30","DOI":"10.1007\/978-3-319-89963-3_30"},{"key":"1155_CR59","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) Proceedings of the CAV. LNCS, vol.\u00a08044, pp. 36\u201352. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_2","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"1155_CR60","doi-asserted-by":"publisher","unstructured":"Helm, D., K\u00fcbler, F., Reif, M., Eichberg, M., Mezini, M.: Modular collaborative program analysis in OPAL. In: Proceedings of the FSE, pp. 184\u2013196. ACM (2020). https:\/\/doi.org\/10.1145\/3368089.3409765","DOI":"10.1145\/3368089.3409765"},{"key":"1155_CR61","doi-asserted-by":"publisher","unstructured":"Hol\u00edk, L., Kotoun, M., Peringer, P., Sokov\u00e1, V., Trt\u00edk, M., Vojnar, T.: Predator shape analysis tool suite. In: Proceedings of the HVC. LNCS, vol. 10028, pp. 202\u2013209 (2016). https:\/\/doi.org\/10.1007\/978-3-319-49052-6_13","DOI":"10.1007\/978-3-319-49052-6_13"},{"key":"1155_CR62","doi-asserted-by":"publisher","unstructured":"Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification. In: Proceedings of the ASE, pp.\u00a01\u20136. IEEE (2008). https:\/\/doi.org\/10.1109\/ASE.2008.9","DOI":"10.1109\/ASE.2008.9"},{"key":"1155_CR63","doi-asserted-by":"publisher","unstructured":"Huster, S., Str\u00f6bele, J., Ruf, J., Kropf, T., Rosenstiel, W.: Using robustness testing to handle incomplete verification results when combining verification and testing techniques. In: Yevtushenko, N., Cavalli, A.R., Yenig\u00fcn, H. (eds.) Proceedings of the ICTSS. LNCS, vol. 10533, pp. 54\u201370. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-67549-7_4","DOI":"10.1007\/978-3-319-67549-7_4"},{"key":"1155_CR64","doi-asserted-by":"publisher","unstructured":"Inkumsah, K., Xie, T.: Improving structural testing of object-oriented programs via integrating evolutionary testing and symbolic execution. In: Proceedings of the ASE, pp. 297\u2013306. IEEE (2008). https:\/\/doi.org\/10.1109\/ASE.2008.40","DOI":"10.1109\/ASE.2008.40"},{"key":"1155_CR65","doi-asserted-by":"publisher","unstructured":"Jakobs, M.: Coveritest with dynamic partitioning of the iteration time limit (competition contribution). In: Wehrheim, H., Cabot, J. (eds.) Proceedings of the FASE. LNCS, vol. 12076, pp. 540\u2013544. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45234-6_30","DOI":"10.1007\/978-3-030-45234-6_30"},{"key":"1155_CR66","doi-asserted-by":"publisher","unstructured":"Jakobs, M., Richter, C.: Coveritest with adaptive time scheduling (competition contribution). In: Guerra, E., Stoelinga, M. (eds.) Proceedings of the FASE. LNCS, vol. 12649, pp. 358\u2013362. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-71500-7_18","DOI":"10.1007\/978-3-030-71500-7_18"},{"key":"1155_CR67","doi-asserted-by":"publisher","unstructured":"Jakobs, M., Wehrheim, H.: Compact Proof Witnesses. In: Barrett, C.W., Davies, M., Kahsai, T. (eds.) Proceedings of the NFM. LNCS, vol. 10227, pp. 389\u2013403 (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_28","DOI":"10.1007\/978-3-319-57288-8_28"},{"key":"1155_CR68","doi-asserted-by":"publisher","unstructured":"Jia, Y., Cohen, M.B., Harman, M., Petke, J.: Learning combinatorial interaction test generation strategies using hyperheuristic search. In: Proceedings of the ICSE, pp. 540\u2013550. IEEE (2015). https:\/\/doi.org\/10.1109\/ICSE.2015.71","DOI":"10.1109\/ICSE.2015.71"},{"key":"1155_CR69","doi-asserted-by":"publisher","unstructured":"Jovanovic, D., Dutertre, B.: Property-directed k-induction. In: Piskac, R., Talupur, M. (eds.) FMCAD, pp. 85\u201392. IEEE (2016). https:\/\/doi.org\/10.1109\/FMCAD.2016.7886665","DOI":"10.1109\/FMCAD.2016.7886665"},{"key":"1155_CR70","doi-asserted-by":"publisher","unstructured":"Kroening, D., Groce, A., Clarke, E.M.: Counterexample guided abstraction refinement via program execution. In: Davies, J., Schulte, W., Barnett, M. (eds.) Proceedings of the ICFEM. LNCS, vol.\u00a03308, pp. 224\u2013238. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-30482-1_23","DOI":"10.1007\/978-3-540-30482-1_23"},{"key":"1155_CR71","doi-asserted-by":"publisher","unstructured":"Liu, D., Ernst, G., Murray, T., Rubinstein, B.I.P.: LEGION: best-first concolic testing. In: Proceedings of the ASE, pp. 54\u201365. IEEE (2020). https:\/\/doi.org\/10.1145\/3324884.3416629","DOI":"10.1145\/3324884.3416629"},{"key":"1155_CR72","doi-asserted-by":"publisher","unstructured":"Liu, D., Ernst, G., Murray, T., Rubinstein, B.I.P.: Legion: Best-first concolic testing (competition contribution). In: Wehrheim, H., Cabot, J. (eds.) Proceedings of the TACAS. LNCS, vol. 12076, pp. 545\u2013549. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45234-6_31","DOI":"10.1007\/978-3-030-45234-6_31"},{"key":"1155_CR73","doi-asserted-by":"publisher","unstructured":"Majumdar, R., Sen, K.: Hybrid concolic testing. In: Proceedings of the ICSE, pp. 416\u2013426. IEEE (2007). https:\/\/doi.org\/10.1109\/ICSE.2007.41","DOI":"10.1109\/ICSE.2007.41"},{"key":"1155_CR74","doi-asserted-by":"publisher","unstructured":"Marques, F., Santos, J.F., Santos, N., Ad\u00e3o, P.: Concolic execution for webassembly. In: Ali, K., Vitek, J. (eds.) Proceedings of the ECOOP. LIPIcs, vol.\u00a0222, pp. 11:1\u201311:29. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2022.11","DOI":"10.4230\/LIPIcs.ECOOP.2022.11"},{"key":"1155_CR75","doi-asserted-by":"publisher","unstructured":"Mukherjee, R., Schrammel, P., Haller, L., Kroening, D., Melham, T.: Lifting CDCL to template-based abstract domains for program verification. In: D\u2019Souza, D., Kumar, K.N. (eds.) Proceedings of the ATVA. LNCS, vol. 10482, pp. 307\u2013326. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_21","DOI":"10.1007\/978-3-319-68167-2_21"},{"key":"1155_CR76","doi-asserted-by":"publisher","unstructured":"Noller, Y., Kersten, R., Pasareanu, C.S.: Badger: complexity analysis with fuzzing and symbolic execution. In: Proceedings of the ISSTA, pp. 322\u2013332. ACM (2018). https:\/\/doi.org\/10.1145\/3213846.3213868","DOI":"10.1145\/3213846.3213868"},{"key":"1155_CR77","doi-asserted-by":"publisher","unstructured":"Nori, A.V., Rajamani, S.K., Tetali, S., Thakur, A.V.: The YogiProject: software property checking via static analysis and testing. In: Kowalewski, S., Philippou, A. (eds.) Proceedings of the TACAS. LNCS, vol.\u00a05505, pp. 178\u2013181. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_17","DOI":"10.1007\/978-3-642-00768-2_17"},{"issue":"1","key":"1155_CR78","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., Wehrheim, H.: Algorithm selection for software validation based on graph kernels. JASE 27(1), 153\u2013186 (2020). https:\/\/doi.org\/10.1007\/s10515-020-00270-x","journal-title":"JASE"},{"key":"1155_CR79","doi-asserted-by":"publisher","unstructured":"Sen, K., Agha, G.: CUTE and jcute: concolic unit testing and explicit path model-checking tools. In: Ball, T., Jones, R.B. (eds.) Proceedings of the CAV. LNCS, vol.\u00a04144, pp. 419\u2013423. Springer (2006). https:\/\/doi.org\/10.1007\/11817963_38","DOI":"10.1007\/11817963_38"},{"key":"1155_CR80","doi-asserted-by":"publisher","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Wermelinger, M., Gall, H.C. (eds.) Proceedings of the ESES\/FSE, pp. 263\u2013272. ACM (2005). https:\/\/doi.org\/10.1145\/1081706.1081750","DOI":"10.1145\/1081706.1081750"},{"key":"1155_CR81","doi-asserted-by":"crossref","unstructured":"Stephens, N., Grosen, J., Salls, C., Dutcher, A., Wang, R., Corbetta, J., Shoshitaishvili, Y., Kruegel, C., Vigna, G.: Driller: augmenting fuzzing through selective symbolic execution. In: Proceedings of the NDSS. The Internet Society (2016). https:\/\/www.ndss-symposium.org\/wp-content\/uploads\/2017\/09\/driller-augmenting-fuzzing-through-selective-symbolic-execution.pdf","DOI":"10.14722\/ndss.2016.23368"},{"key":"1155_CR82","doi-asserted-by":"publisher","unstructured":"Tillmann, N., de\u00a0Halleux, J.: Pex-white box test generation for .net. In: Beckert, B., H\u00e4hnle, R. (eds.) Proceedings of the TAP. LNCS, vol.\u00a04966, pp. 134\u2013153. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-79124-9_10","DOI":"10.1007\/978-3-540-79124-9_10"},{"key":"1155_CR83","doi-asserted-by":"publisher","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Usable verification of object-oriented programs by combining static and dynamic techniques. In: Proceedings of the SEFM. LNCS, vol.\u00a07041, pp. 382\u2013398. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-24690-6_26","DOI":"10.1007\/978-3-642-24690-6_26"},{"key":"1155_CR84","doi-asserted-by":"publisher","unstructured":"Tulsian, V., Kanade, A., Kumar, R., Lal, A., Nori, A.V.: MUX: Algorithm selection for software model checkers. In: Proceedings of the MSR, pp. 132\u2014141. ACM (2014). https:\/\/doi.org\/10.1145\/2597073.2597080","DOI":"10.1145\/2597073.2597080"},{"key":"1155_CR85","doi-asserted-by":"publisher","unstructured":"Yin, L., Dong, W., Liu, W., Wang, J.: Parallel refinement for multi-threaded program verification. In: Proceedings of the ICSE, pp. 643\u2013653. IEEE (2019). https:\/\/doi.org\/10.1109\/ICSE.2019.00074","DOI":"10.1109\/ICSE.2019.00074"},{"key":"1155_CR86","doi-asserted-by":"publisher","unstructured":"Yorsh, G., Ball, T., Sagiv, M.: Testing, abstraction, theorem proving: Better together! In: Proceedings of the ISSTA, pp. 145\u2013156. ACM (2006). https:\/\/doi.org\/10.1145\/1146238.1146255","DOI":"10.1145\/1146238.1146255"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-024-01155-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-024-01155-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-024-01155-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,20]],"date-time":"2024-07-20T04:16:14Z","timestamp":1721448974000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-024-01155-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,3,19]]},"references-count":86,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["1155"],"URL":"https:\/\/doi.org\/10.1007\/s10270-024-01155-3","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2024,3,19]]},"assertion":[{"value":"28 February 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 October 2023","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 January 2024","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 March 2024","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}