{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:03:55Z","timestamp":1776373435640,"version":"3.51.2"},"reference-count":128,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2021,4,25]],"date-time":"2021-04-25T00:00:00Z","timestamp":1619308800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,4,25]],"date-time":"2021-04-25T00:00:00Z","timestamp":1619308800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005714","name":"Technische Universit\u00e4t Darmstadt","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005714","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":[[2021,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Testing is a widely applied technique to evaluate software quality, and coverage criteria are often used to assess the adequacy of a generated test suite. However, manually constructing an adequate test suite is typically too expensive, and numerous techniques for automatic test-suite generation were proposed. All of them come with different strengths. To build stronger test-generation tools, different techniques should be combined. In this paper, we study cooperative combinations of verification approaches for test generation, which exchange high-level information. We present <jats:sc>CoVeriTest<\/jats:sc>, a hybrid technique for test-suite generation. <jats:sc>CoVeriTest<\/jats:sc> iteratively applies different conditional model checkers and allows users to adjust the level of cooperation and to configure individual time limits for each conditional model checker. In our experiments, we systematically study different <jats:sc>CoVeriTest<\/jats:sc> cooperation setups, which either use combinations of explicit-state model checking and predicate abstraction, or bounded model checking and symbolic execution. A comparison with state-of-the-art test-generation tools reveals that <jats:sc>CoVeriTest<\/jats:sc> achieves higher coverage for many programs (about 15%).<\/jats:p>","DOI":"10.1007\/s10009-020-00587-8","type":"journal-article","created":{"date-parts":[[2021,4,25]],"date-time":"2021-04-25T10:13:30Z","timestamp":1619345610000},"page":"313-333","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Cooperative verifier-based testing with CoVeriTest"],"prefix":"10.1007","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4832-7662","authenticated-orcid":false,"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marie-Christine","family":"Jakobs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,4,25]]},"reference":[{"key":"587_CR1","volume-title":"Compilers: Principles, Techniques, and Tools","author":"AV Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley, Reading (1986)"},{"key":"587_CR2","doi-asserted-by":"publisher","unstructured":"Albarghouthi, A., Gurfinkel, A., Chechik, M.: From under-approximations to over-approximations and back. In: Proceedings of TACAS, LNCS, vol. 7214, pp. 157\u2013172. Springer, Berlin (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_12","DOI":"10.1007\/978-3-642-28756-5_12"},{"key":"587_CR3","doi-asserted-by":"publisher","unstructured":"Albert, E., Puebla, G., Hermenegildo, M.V.: Abstraction-carrying code. In: Proceedings of LPAR, LNCS, vol. 3452, pp. 380\u2013397. Springer, Berlin (2004). https:\/\/doi.org\/10.1007\/978-3-540-32275-7_25","DOI":"10.1007\/978-3-540-32275-7_25"},{"key":"587_CR4","doi-asserted-by":"publisher","unstructured":"Apel, S., Beyer, D., Friedberger, K., Raimondi, F., von Rhein, A.: Domain types: abstract-domain selection based on variable usage. In: Proceedings of HVC, LNCS\u00a08244, pp. 262\u2013278. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-319-03077-7","DOI":"10.1007\/978-3-319-03077-7"},{"key":"587_CR5","doi-asserted-by":"publisher","unstructured":"Aquino, A., Bianchi, F.A., Chen, M., Denaro, G., Pezz\u00e8, M.: Reusing constraint proofs in program analysis. In: Proceedings of ISSTA, pp. 305\u2013315. ACM, New York (2015). https:\/\/doi.org\/10.1145\/2771783.2771802","DOI":"10.1145\/2771783.2771802"},{"key":"587_CR6","doi-asserted-by":"publisher","unstructured":"Baars, A.I., Harman, M., Hassoun, Y., Lakhotia, K., McMinn, P., Tonella, P., Vos, T.E.J.: Symbolic search-based testing. In: Proceedings of ASE, pp. 53\u201362. IEEE (2011). https:\/\/doi.org\/10.1109\/ASE.2011.6100119","DOI":"10.1109\/ASE.2011.6100119"},{"key":"587_CR7","doi-asserted-by":"publisher","unstructured":"Baluda, M.: EvoSE: evolutionary symbolic execution. In: Proceedings of A-TEST, pp. 16\u201319. ACM, New York (2015). https:\/\/doi.org\/10.1145\/2804322.2804325","DOI":"10.1145\/2804322.2804325"},{"key":"587_CR8","doi-asserted-by":"publisher","unstructured":"Beckman, N., Nori, A.V., Rajamani, S.K., Simmons, R.J.: Proofs from tests. In: Proceedings of ISSTA, pp. 3\u201314. ACM, New York (2008). https:\/\/doi.org\/10.1145\/1390630.1390634","DOI":"10.1145\/1390630.1390634"},{"key":"587_CR9","doi-asserted-by":"publisher","unstructured":"Besson, F., Cornilleau, P., Jensen, T.P.: Result certification of static program analysers with automated theorem provers. In: Proceedings of VSTTE, LNCS, vol. 8164, pp. 304\u2013325. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-54108-7_16","DOI":"10.1007\/978-3-642-54108-7_16"},{"issue":"3","key":"587_CR10","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/j.tcs.2006.08.012","volume":"364","author":"F Besson","year":"2006","unstructured":"Besson, F., Jensen, T.P., Pichardie, D.: Proof-carrying code from certified abstract interpretation and fixpoint compression. TCS 364(3), 273\u2013291 (2006). https:\/\/doi.org\/10.1016\/j.tcs.2006.08.012","journal-title":"TCS"},{"key":"587_CR11","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Automatic verification of C and Java programs: SV-COMP 2019. In: Proceedings of TACAS (3), LNCS, vol. 11429, pp. 133\u2013155. Springer, Berlin (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_9","DOI":"10.1007\/978-3-030-17502-3_9"},{"key":"587_CR12","volume-title":"First international competition on software testing (Test-Comp 2019)","author":"D Beyer","year":"2020","unstructured":"Beyer, D.: First international competition on software testing (Test-Comp 2019). Int. J. Softw. Tools Technol, Transf (2020)"},{"key":"587_CR13","doi-asserted-by":"publisher","unstructured":"Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating tests from counterexamples. In: Proceedings of ICSE, pp. 326\u2013335. IEEE (2004). https:\/\/doi.org\/10.1109\/ICSE.2004.1317455","DOI":"10.1109\/ICSE.2004.1317455"},{"key":"587_CR14","doi-asserted-by":"publisher","unstructured":"Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: The Blast query language for software verification. In: Proceedings of SAS, LNCS, vol. 3148, pp. 2\u201318. Springer, Berlin (2004). https:\/\/doi.org\/10.1007\/978-3-540-27864-1_2","DOI":"10.1007\/978-3-540-27864-1_2"},{"key":"587_CR15","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 ISoLA, LNCS, vol. 11245, pp. 144\u2013159. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_11","DOI":"10.1007\/978-3-030-03421-4_11"},{"key":"587_CR16","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: exchanging verification results between verifiers. In: Proceedings of FSE, pp. 326\u2013337. ACM, New York (2016). https:\/\/doi.org\/10.1145\/2950290.2950351","DOI":"10.1145\/2950290.2950351"},{"key":"587_CR17","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Stahlbauer, A.: Witness validation and stepwise testification across software verifiers. In: Proceedings of FSE, pp. 721\u2013733. ACM, New York (2015). https:\/\/doi.org\/10.1145\/2786805.2786867","DOI":"10.1145\/2786805.2786867"},{"key":"587_CR18","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Lemberger, T., Tautschnig, M.: Tests from witnesses: execution-based validation of verification results. In: Proceedings of TAP, LNCS, vol. 10889, pp. 3\u201323. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-92994-1_1","DOI":"10.1007\/978-3-319-92994-1_1"},{"key":"587_CR19","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction with continuously-refined invariants. In: Proceedings of CAV, LNCS, vol. 9206, pp. 622\u2013640. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_42","DOI":"10.1007\/978-3-319-21690-4_42"},{"issue":"3","key":"587_CR20","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/s10817-017-9432-6","volume":"60","author":"D Beyer","year":"2018","unstructured":"Beyer, D., Dangl, M., Wendler, P.: A unifying view on SMT-based software verification. J. Autom. Reason. 60(3), 299\u2013335 (2018). https:\/\/doi.org\/10.1007\/s10817-017-9432-6","journal-title":"J. Autom. Reason."},{"key":"587_CR21","doi-asserted-by":"publisher","unstructured":"Beyer, D., Friedberger, K.: Domain-independent multi-threaded software model checking. In: Proceedings of ASE, pp. 634\u2013644. ACM, New York (2018). https:\/\/doi.org\/10.1145\/3238147.3238195","DOI":"10.1145\/3238147.3238195"},{"key":"587_CR22","doi-asserted-by":"publisher","unstructured":"Beyer, D., Gulwani, S., Schmidt, D.: Combining model checking and data-flow analysis. In: Clarke, E.M., Henzinger, T.A., Veith, H. (eds.) Handbook on Model Checking, pp. 493\u2013540. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_16","DOI":"10.1007\/978-3-319-10575-8_16"},{"key":"587_CR23","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: Proceedings of FSE. ACM, New York (2012). https:\/\/doi.org\/10.1145\/2393596.2393664","DOI":"10.1145\/2393596.2393664"},{"key":"587_CR24","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Program analysis with dynamic precision adjustment. In: Proceedings of ASE, pp. 29\u201338. IEEE (2008). https:\/\/doi.org\/10.1109\/ASE.2008.13","DOI":"10.1109\/ASE.2008.13"},{"key":"587_CR25","doi-asserted-by":"publisher","unstructured":"Beyer, D., Holzer, A., Tautschnig, M., Veith, H.: Information reuse for multi-goal reachability analyses. In: Proceedings of ESOP, LNCS, vol. 7792, pp. 472\u2013491. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_26","DOI":"10.1007\/978-3-642-37036-6_26"},{"key":"587_CR26","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jakobs, M.C.: CoVeriTest: cooperative verifier-based testing. In: Proceedings of FASE, LNCS, vol. 11424, pp. 389\u2013408. Springer, Berlin (2019). https:\/\/doi.org\/10.1007\/978-3-030-16722-6_23","DOI":"10.1007\/978-3-030-16722-6_23"},{"key":"587_CR27","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.3666060","author":"D Beyer","year":"2020","unstructured":"Beyer, D., Jakobs, M.C.: Replication package for article \u2018Cooperative, verifier-based testing with CoVeriTest\u2019 in STTT. Zenodo (2020). https:\/\/doi.org\/10.5281\/zenodo.3666060","journal-title":"Zenodo"},{"key":"587_CR28","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jakobs, M.C., Lemberger, T., Wehrheim, H.: Reducer-based construction of conditional verifiers. In: Proceedings of ICSE, pp. 1182\u20131193. ACM, New York (2018). https:\/\/doi.org\/10.1145\/3180155.3180259","DOI":"10.1145\/3180155.3180259"},{"key":"587_CR29","doi-asserted-by":"publisher","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Proceedings of CAV, LNCS, vol. 6806, pp. 184\u2013190. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"587_CR30","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Proceedings of FMCAD, pp. 189\u2013197. FMCAD (2010)"},{"key":"587_CR31","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lemberger, T.: Symbolic execution with CEGAR. In: Proceedings of ISoLA, LNCS, vol. 9952, pp. 195\u2013211. Springer, Berlin (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_14","DOI":"10.1007\/978-3-319-47166-2_14"},{"key":"587_CR32","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lemberger, T.: Software verification: testing vs. model checking. In: Proceedings of HVC, LNCS, vol. 10629, pp. 99\u2013114. Springer, Berlin (2017). https:\/\/doi.org\/10.1007\/978-3-319-70389-3_7","DOI":"10.1007\/978-3-319-70389-3_7"},{"key":"587_CR33","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lemberger, T.: Conditional testing: Off-the-shelf combination of test-case generators. In: Proceedings ATVA, LNCS, vol. 11781, pp. 189\u2013208. Springer, Berlin (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_11","DOI":"10.1007\/978-3-030-31784-3_11"},{"key":"587_CR34","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lemberger, T.: TestCov: Robust test-suite execution and coverage measurement. In: Proceedings of ASE, pp. 1074\u20131077. IEEE (2019). https:\/\/doi.org\/10.1109\/ASE.2019.00105","DOI":"10.1109\/ASE.2019.00105"},{"key":"587_CR35","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S.: Explicit-state software model checking based on CEGAR and interpolation. In: Proceedings of FASE, LNCS, vol. 7793, pp. 146\u2013162. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-37057-1_11","DOI":"10.1007\/978-3-642-37057-1_11"},{"key":"587_CR36","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S., Novikov, E., Stahlbauer, A., Wendler, P.: Precision reuse for efficient regression verification. In: Proceedings of FSE, pp. 389\u2013399. ACM, New York (2013). https:\/\/doi.org\/10.1145\/2491411.2491429","DOI":"10.1145\/2491411.2491429"},{"key":"587_CR37","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Refinement selection. In: Proceedings of SPIN, LNCS, vol. 9232, pp. 20\u201338. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-319-23404-5_3","DOI":"10.1007\/978-3-319-23404-5_3"},{"key":"587_CR38","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Sliced path prefixes: an effective method to enable refinement selection. In: Proceedings of FORTE, LNCS, vol. 9039, pp. 228\u2013243. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-319-19195-9_15","DOI":"10.1007\/978-3-319-19195-9_15"},{"issue":"1","key":"587_CR39","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. Transfer 21(1), 1\u201329 (2019). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"587_CR40","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/j.scico.2013.11.026","volume":"97","author":"D Bianculli","year":"2015","unstructured":"Bianculli, D., Filieri, A., Ghezzi, C., Mandrioli, D.: Syntactic-semantic incrementality for agile verification. SCICO 97, 47\u201354 (2015). https:\/\/doi.org\/10.1016\/j.scico.2013.11.026","journal-title":"Syntactic-semantic incrementality for agile verification. SCICO"},{"key":"587_CR41","doi-asserted-by":"publisher","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proceedings of TACAS, LNCS, vol. 1579, pp. 193\u2013207. Springer, Berlin (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"key":"587_CR42","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: Proceedings of 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":"587_CR43","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of OSDI, pp. 209\u2013224. USENIX Association (2008)"},{"issue":"2","key":"587_CR44","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. CACM 56(2), 82\u201390 (2013). https:\/\/doi.org\/10.1145\/2408776.2408795","journal-title":"CACM"},{"key":"587_CR45","doi-asserted-by":"publisher","unstructured":"Carroll, M.D., Ryder, B.G.: Incremental data flow analysis via dominator and attribute updates. In: Proceedings of POPL, pp. 274\u2013284. ACM, New York (1988). https:\/\/doi.org\/10.1145\/73560.73584","DOI":"10.1145\/73560.73584"},{"key":"587_CR46","doi-asserted-by":"publisher","unstructured":"Chaieb, A.: Proof-producing program analysis. In: Proceedings of ICTAC, LNCS, vol. 4281, pp. 287\u2013301. Springer, Berlin (2006). https:\/\/doi.org\/10.1007\/11921240_20","DOI":"10.1007\/11921240_20"},{"key":"587_CR47","doi-asserted-by":"publisher","unstructured":"Chalupa, M., Vitovsk\u00e1, M., Strejcek, J.: Symbiotic 5: boosted instrumentation (competition contribution). In: Proceedings of TACAS, LNCS, vol. 10806, pp. 442\u2013446. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_29","DOI":"10.1007\/978-3-319-89963-3_29"},{"key":"587_CR48","doi-asserted-by":"publisher","unstructured":"Chebaro, O., Kosmatov, N., Giorgetti, A., Julliand, J.: Program slicing enhances a verification technique combining static and dynamic analysis. In: Proceedings of SAC, pp. 1284\u20131291. ACM, New York (2012). https:\/\/doi.org\/10.1145\/2245276.2231980","DOI":"10.1145\/2245276.2231980"},{"issue":"2\u20133","key":"587_CR49","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/s10994-009-5127-5","volume":"76","author":"W Cheng","year":"2009","unstructured":"Cheng, W., H\u00fcllermeier, E.: Combining instance-based learning and logistic regression for multilabel classification. Mach. Learn. 76(2\u20133), 211\u2013225 (2009). https:\/\/doi.org\/10.1007\/s10994-009-5127-5","journal-title":"Mach. Learn."},{"key":"587_CR50","doi-asserted-by":"publisher","unstructured":"Chowdhury, A.B., Medicherla, R.K., Venkatesh, R.: VeriFuzz: program aware fuzzing (competition contribution). In: Proceedings of TACAS, part 3, LNCS, vol. 11429, pp. 244\u2013249. Springer, Berlin (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_22","DOI":"10.1007\/978-3-030-17502-3_22"},{"key":"587_CR51","doi-asserted-by":"publisher","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Guiding dynamic symbolic execution toward unverified program executions. In: Proceedings of ICSE, pp. 144\u2013155. ACM, New York (2016). https:\/\/doi.org\/10.1145\/2884781.2884843","DOI":"10.1145\/2884781.2884843"},{"issue":"4","key":"587_CR52","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/1713254.1713257","volume":"43","author":"L Ciortea","year":"2009","unstructured":"Ciortea, L., Zamfir, C., Bucur, S., Chipounov, V., Candea, G.: Cloud9: a software testing service. ACM SIGOPS Oper. Syst. Rev. 43(4), 5\u201310 (2009). https:\/\/doi.org\/10.1145\/1713254.1713257","journal-title":"ACM SIGOPS Oper. Syst. Rev."},{"key":"587_CR53","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Proceedings CAV, LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Berlin (2000). https:\/\/doi.org\/10.1007\/10722167_15","DOI":"10.1007\/10722167_15"},{"key":"587_CR54","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Handbook of Model Checking","author":"EM 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"},{"key":"587_CR55","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Kr\u00f6ning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Proceedings of TACAS, LNCS\u00a02988, pp. 168\u2013176. Springer, Berlin (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"587_CR56","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Systematic design of program-analysis frameworks. In: Proceedings of POPL, pp. 269\u2013282. ACM, New York (1979). https:\/\/doi.org\/10.1145\/567752.567778","DOI":"10.1145\/567752.567778"},{"key":"587_CR57","doi-asserted-by":"publisher","unstructured":"Csallner, C., Smaragdakis, Y.: Check \u2018n\u2019 crash: combining static checking and testing. In: Proceedings of ICSE, pp. 422\u2013431. ACM, New York (2005). https:\/\/doi.org\/10.1145\/1062455.1062533","DOI":"10.1145\/1062455.1062533"},{"key":"587_CR58","doi-asserted-by":"publisher","unstructured":"Czech, M., H\u00fcllermeier, E., Jakobs, M., Wehrheim, H.: Predicting rankings of software verification tools. In: Proceedings of SWAN, pp. 23\u201326. ACM, New York (2017). https:\/\/doi.org\/10.1145\/3121257.3121262","DOI":"10.1145\/3121257.3121262"},{"key":"587_CR59","doi-asserted-by":"publisher","unstructured":"Czech, M., Jakobs, M., Wehrheim, H.: Just test what you cannot verify! In: Proceedings of FASE, LNCS, vol. 9033, pp. 100\u2013114. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-662-46675-9_7","DOI":"10.1007\/978-3-662-46675-9_7"},{"key":"587_CR60","doi-asserted-by":"publisher","unstructured":"Daca, P., Gupta, A., Henzinger, T.A.: Abstraction-driven concolic testing. In: Proceedings of VMCAI, LNCS, vol. 9583, pp. 328\u2013347. Springer, Berlin (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_16","DOI":"10.1007\/978-3-662-49122-5_16"},{"key":"587_CR61","doi-asserted-by":"publisher","unstructured":"Demyanova, Y., Pani, T., Veith, H., Zuleger, F.: Empirical software metrics for benchmarking of verification tools. In: Proceedings of CAV, LNCS, vol. 9206, pp. 561\u2013579. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_39","DOI":"10.1007\/978-3-319-21690-4_39"},{"key":"587_CR62","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"issue":"3","key":"587_CR63","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1002\/stvr.402","volume":"19","author":"G Fraser","year":"2009","unstructured":"Fraser, G., Wotawa, F., Ammann, P.: Testing with model checkers: a survey. Softw. Test. Verif. Reliab. 19(3), 215\u2013261 (2009). https:\/\/doi.org\/10.1002\/stvr.402","journal-title":"Softw. Test. Verif. Reliab."},{"key":"587_CR64","doi-asserted-by":"publisher","unstructured":"Galeotti, J.P., Fraser, G., Arcuri, A.: Improving search-based test suite generation with dynamic symbolic execution. In: Proceedings of ISSRE, pp. 360\u2013369. IEEE (2013). https:\/\/doi.org\/10.1109\/ISSRE.2013.6698889","DOI":"10.1109\/ISSRE.2013.6698889"},{"key":"587_CR65","doi-asserted-by":"publisher","unstructured":"Gargantini, A., Vavassori, P.: Using decision trees to aid algorithm selection in combinatorial interaction tests generation. In: Proceedings of ICST, pp. 1\u201310. IEEE (2015). https:\/\/doi.org\/10.1109\/ICSTW.2015.7107442","DOI":"10.1109\/ICSTW.2015.7107442"},{"key":"587_CR66","doi-asserted-by":"publisher","unstructured":"Ge, X., Taneja, K., Xie, T., Tillmann, N.: DyTa: dynamic symbolic execution guided with static verification results. In: Proceedings of ICSE, pp. 992\u2013994. ACM, New York (2011). https:\/\/doi.org\/10.1145\/1985793.1985971","DOI":"10.1145\/1985793.1985971"},{"key":"587_CR67","volume-title":"Fundamentals of Software Engineering","author":"C Ghezzi","year":"2003","unstructured":"Ghezzi, C., Jazayeri, M., Mandrioli, D.: Fundamentals of Software Engineering, 2nd edn. Prentice Hall, Englewood Cliffs (2003)","edition":"2"},{"key":"587_CR68","doi-asserted-by":"publisher","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: Dart: directed automated random testing. In: Proceedings of PLDI, pp. 213\u2013223. ACM, New York (2005). https:\/\/doi.org\/10.1145\/1065010.1065036","DOI":"10.1145\/1065010.1065036"},{"key":"587_CR69","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. In: Proceedings of NDSS. The Internet Society (2008)"},{"key":"587_CR70","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: Proceedings of POPL, pp. 43\u201356. ACM, New York (2010). https:\/\/doi.org\/10.1145\/1706299.1706307","DOI":"10.1145\/1706299.1706307"},{"key":"587_CR71","doi-asserted-by":"publisher","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with Pvs. In: Proceedings of CAV, LNCS, vol. 1254, pp. 72\u201383. Springer, Berlin (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_10","DOI":"10.1007\/3-540-63166-6_10"},{"key":"587_CR72","doi-asserted-by":"publisher","unstructured":"Groce, A., Zhang, C., Eide, E., Chen, Y., Regehr, J.: Swarm testing. In: Proceedings of ISSTA, pp. 78\u201388. ACM, New York (2012). https:\/\/doi.org\/10.1145\/2338965.2336763","DOI":"10.1145\/2338965.2336763"},{"key":"587_CR73","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: Proceedings of FSE, pp. 117\u2013127. ACM, New York (2006). https:\/\/doi.org\/10.1145\/1181775.1181790","DOI":"10.1145\/1181775.1181790"},{"key":"587_CR74","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Proceedings of POPL, pp. 232\u2013244. ACM, New York (2004). https:\/\/doi.org\/10.1145\/964001.964021","DOI":"10.1145\/964001.964021"},{"key":"587_CR75","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G.C., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Proceedings of CAV, LNCS, vol. 2404, pp. 526\u2013538. Springer, Berlin (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_45","DOI":"10.1007\/3-540-45657-0_45"},{"key":"587_CR76","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sanvido, M.A.A.: Extreme model checking. In: Verification: Theory and Practice, pp. 332\u2013358 (2003). https:\/\/doi.org\/10.1007\/978-3-540-39910-0_16","DOI":"10.1007\/978-3-540-39910-0_16"},{"key":"587_CR77","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of POPL, pp. 58\u201370. ACM, New York (2002). https:\/\/doi.org\/10.1145\/503272.503279","DOI":"10.1145\/503272.503279"},{"key":"587_CR78","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 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":"587_CR79","doi-asserted-by":"publisher","unstructured":"Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: FShell: Systematic test case generation for dynamic analysis and measurement. In: Proceedings of CAV, LNCS, vol. 5123, pp. 209\u2013213. Springer, Berlin (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_20","DOI":"10.1007\/978-3-540-70545-1_20"},{"key":"587_CR80","doi-asserted-by":"publisher","unstructured":"Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: Query-driven program testing. In: Proceedings of VMCAI, LNCS, vol. 5403, pp. 151\u2013166. Springer, Berlin (2009). https:\/\/doi.org\/10.1007\/978-3-540-93900-9_15","DOI":"10.1007\/978-3-540-93900-9_15"},{"key":"587_CR81","doi-asserted-by":"publisher","unstructured":"Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: How did you specify your test suite. In: Proceedings of ASE, pp. 407\u2013416. ACM, New York (2010). https:\/\/doi.org\/10.1145\/1858996.1859084","DOI":"10.1145\/1858996.1859084"},{"key":"587_CR82","doi-asserted-by":"publisher","unstructured":"Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification. In: Proceedings of ASE, pp. 1\u20136. IEEE (2008). https:\/\/doi.org\/10.1109\/ASE.2008.9","DOI":"10.1109\/ASE.2008.9"},{"key":"587_CR83","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 ASE, pp. 297\u2013306. IEEE (2008). https:\/\/doi.org\/10.1109\/ASE.2008.40","DOI":"10.1109\/ASE.2008.40"},{"key":"587_CR84","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-020-00572-1","author":"MC Jakobs","year":"2020","unstructured":"Jakobs, M.C.: CoVeriTest: Interleaving value and predicate analysis for test-case generation (competition contribution). Int. J. Softw. Tools Technol. Transf. (2020). https:\/\/doi.org\/10.1007\/s10009-020-00572-1","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"587_CR85","doi-asserted-by":"publisher","unstructured":"Jakobs, M.C.: CoVeriTest with dynamic partitioning of the iteration time limit (competition contribution). In: Proceedings of FASE, LNCS, vol. 12076, pp. 540\u2013544. Springer, Berlin (2020). https:\/\/doi.org\/10.1007\/978-3-030-45234-6_30","DOI":"10.1007\/978-3-030-45234-6_30"},{"key":"587_CR86","doi-asserted-by":"publisher","unstructured":"Jakobs, M.C., Wehrheim, H.: Certification for configurable program analysis. In: Proceedings of SPIN, pp. 30\u201339. ACM, New York (2014). https:\/\/doi.org\/10.1145\/2632362.2632372","DOI":"10.1145\/2632362.2632372"},{"issue":"2","key":"587_CR87","doi-asserted-by":"publisher","first-page":"7:1","DOI":"10.1145\/3014427","volume":"39","author":"MC Jakobs","year":"2017","unstructured":"Jakobs, M.C., Wehrheim, H.: Programs from proofs: a framework for the safe execution of untrusted software. ACM Trans. Program. Lang. Syst. 39(2), 7:1\u20137:56 (2017). https:\/\/doi.org\/10.1145\/3014427","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"587_CR88","doi-asserted-by":"publisher","unstructured":"Jalote, P., Vangala, V., Singh, T., Jain, P.: Program partitioning: a framework for combining static and dynamic analysis. In: Proceedings of WODA, pp. 11\u201316. ACM, New York (2006). https:\/\/doi.org\/10.1145\/1138912.1138916","DOI":"10.1145\/1138912.1138916"},{"key":"587_CR89","doi-asserted-by":"publisher","first-page":"4","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 (2009). https:\/\/doi.org\/10.1145\/1592434.1592438","journal-title":"ACM Comput. Surv."},{"key":"587_CR90","doi-asserted-by":"publisher","unstructured":"Jia, X., Ghezzi, C., Ying, S.: Enhancing reuse of constraint solutions to improve symbolic execution. In: Proceedings of ISSTA, pp. 177\u2013187. ACM, New York (2015). https:\/\/doi.org\/10.1145\/2771783.2771806","DOI":"10.1145\/2771783.2771806"},{"key":"587_CR91","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 ICSE, pp. 540\u2013550. IEEE (2015). https:\/\/doi.org\/10.1109\/ICSE.2015.71","DOI":"10.1109\/ICSE.2015.71"},{"key":"587_CR92","doi-asserted-by":"publisher","unstructured":"Kim, Y., Xu, Z., Kim, M., Cohen, M.B., Rothermel, G.: Hybrid directed test suite augmentation: an interleaving framework. In: Proceedings of ICST, pp. 263\u2013272. IEEE (2014). https:\/\/doi.org\/10.1109\/ICST.2014.39","DOI":"10.1109\/ICST.2014.39"},{"issue":"7","key":"587_CR93","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976). https:\/\/doi.org\/10.1145\/360248.360252","journal-title":"Commun. ACM"},{"key":"587_CR94","doi-asserted-by":"publisher","unstructured":"Kotthoff, L.: Algorithm selection for combinatorial search problems: a survey. In: Data Mining and Constraint Programming\u2013Foundations of a Cross-Disciplinary Approach, LNCS, vol. 10101, pp. 149\u2013190. Springer, Berlin (2016). https:\/\/doi.org\/10.1007\/978-3-319-50137-6_7","DOI":"10.1007\/978-3-319-50137-6_7"},{"key":"587_CR95","doi-asserted-by":"publisher","unstructured":"Lemieux, C., Sen, K.: FairFuzz: a targeted mutation strategy for increasing greybox fuzz testing coverage. In: Proceedings of ASE, pp. 475\u2013485. ACM, New York (2018). https:\/\/doi.org\/10.1145\/3238147.3238176","DOI":"10.1145\/3238147.3238176"},{"issue":"1","key":"587_CR96","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1186\/s42400-018-0002-y","volume":"1","author":"J Li","year":"2018","unstructured":"Li, J., Zhao, B., Zhang, C.: Fuzzing: a survey. Cybersecurity 1(1), 6 (2018). https:\/\/doi.org\/10.1186\/s42400-018-0002-y","journal-title":"Cybersecurity"},{"key":"587_CR97","doi-asserted-by":"publisher","unstructured":"Li, K., Reichenbach, C., Csallner, C., Smaragdakis, Y.: Residual investigation: predictive and precise bug detection. In: Proceedings of ISSTA, pp. 298\u2013308. ACM, New York (2012). https:\/\/doi.org\/10.1145\/2338965.2336789","DOI":"10.1145\/2338965.2336789"},{"key":"587_CR98","doi-asserted-by":"publisher","unstructured":"Majumdar, R., Sen, K.: Hybrid concolic testing. In: Proceedings of ICSE, pp. 416\u2013426. IEEE (2007). https:\/\/doi.org\/10.1109\/ICSE.2007.41","DOI":"10.1109\/ICSE.2007.41"},{"issue":"2","key":"587_CR99","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":"587_CR100","doi-asserted-by":"publisher","unstructured":"Misailovic, S., Milicevic, A., Petrovic, N., Khurshid, S., Marinov, D.: Parallel test generation and execution with Korat. In: Proceedings of ESEC\/FSE, pp. 135\u2013144. ACM, New York (2007). https:\/\/doi.org\/10.1145\/1287624.1287645","DOI":"10.1145\/1287624.1287645"},{"key":"587_CR101","doi-asserted-by":"publisher","unstructured":"Mudduluru, R., Ramanathan, M.K.: Efficient incremental static analysis using path abstraction. In: Proceedings of FASE, LNCS, vol. 8411, pp. 125\u2013139. Springer, Berlin (2014). https:\/\/doi.org\/10.1007\/978-3-642-54804-8_9","DOI":"10.1007\/978-3-642-54804-8_9"},{"key":"587_CR102","doi-asserted-by":"publisher","unstructured":"Nguyen, T.L., Schrammel, P., Fischer, B., La\u00a0Torre, S., Parlato, G.: Parallel bug-finding in concurrent programs via reduced interleaving instances. In: Proceedings of ASE, pp. 753\u2013764. IEEE (2017). https:\/\/doi.org\/10.1109\/ASE.2017.8115686","DOI":"10.1109\/ASE.2017.8115686"},{"key":"587_CR103","doi-asserted-by":"publisher","unstructured":"Noller, Y., Kersten, R., Pasareanu, C.S.: Badger: Complexity analysis with fuzzing and symbolic execution. In: Proceedings of ISSTA, pp. 322\u2013332. ACM, New York (2018). https:\/\/doi.org\/10.1145\/3213846.3213868","DOI":"10.1145\/3213846.3213868"},{"key":"587_CR104","doi-asserted-by":"publisher","unstructured":"Pacheco, C., Lahiri, S.K., Ernst, M.D., Ball, T.: Feedback-directed random test generation. In: Proceedings of ICSE, pp. 75\u201384. IEEE (2007). https:\/\/doi.org\/10.1109\/ICSE.2007.37","DOI":"10.1109\/ICSE.2007.37"},{"issue":"4","key":"587_CR105","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/s10009-009-0118-1","volume":"11","author":"CS 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":"587_CR106","doi-asserted-by":"publisher","unstructured":"Person, S., Yang, G., Rungta, N., Khurshid, S.: Directed incremental symbolic execution. In: Proceedings of PLDI, pp. 504\u2013515. ACM, New York (2011). https:\/\/doi.org\/10.1145\/1993498.1993558","DOI":"10.1145\/1993498.1993558"},{"key":"587_CR107","doi-asserted-by":"publisher","unstructured":"Post, H., Sinz, C., Kaiser, A., Gorges, T.: Reducing false positives by combining abstract interpretation and bounded model checking. In: Proceedings of ASE, pp. 188\u2013197. IEEE (2008). https:\/\/doi.org\/10.1109\/ASE.2008.29","DOI":"10.1109\/ASE.2008.29"},{"key":"587_CR108","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0065-2458(08)60520-3","volume":"15","author":"JR Rice","year":"1976","unstructured":"Rice, J.R.: The algorithm selection problem. Adv. Comput. 15, 65\u2013118 (1976). https:\/\/doi.org\/10.1016\/S0065-2458(08)60520-3","journal-title":"Adv. Comput."},{"key":"587_CR109","doi-asserted-by":"publisher","unstructured":"Richter, C., Wehrheim, H.: PeSCo: predicting sequential combinations of verifiers (competition contribution). In: Proceedings of TACAS, LNCS, vol. 11429, pp. 229\u2013233. Springer, Berlin (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_19","DOI":"10.1007\/978-3-030-17502-3_19"},{"issue":"3\u20134","key":"587_CR110","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1023\/B:JARS.0000021015.15794.82","volume":"31","author":"E Rose","year":"2003","unstructured":"Rose, E.: Lightweight bytecode verification. J. Autom. Reason. 31(3\u20134), 303\u2013334 (2003). https:\/\/doi.org\/10.1023\/B:JARS.0000021015.15794.82","journal-title":"J. Autom. Reason."},{"key":"587_CR111","doi-asserted-by":"publisher","unstructured":"Rothenberg, B., Dietsch, D., Heizmann, M.: Incremental verification using trace abstraction. In: Proceedings of SAS, LNCS, vol. 11002, pp. 364\u2013382. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-99725-4_22","DOI":"10.1007\/978-3-319-99725-4_22"},{"key":"587_CR112","doi-asserted-by":"publisher","unstructured":"Ryder, B.G.: Incremental data flow analysis. In: Proceedings of POPL, pp. 167\u2013176. ACM Press, New York (1983). https:\/\/doi.org\/10.1145\/567067.567084","DOI":"10.1145\/567067.567084"},{"key":"587_CR113","doi-asserted-by":"publisher","unstructured":"Sakti, A., Gu\u00e9h\u00e9neuc, Y., Pesant, G.: Boosting search based testing by using constraint based testing. In: Proceedings of SSBSE, LNCS, vol. 7515, pp. 213\u2013227. Springer, Berlin (2012). https:\/\/doi.org\/10.1007\/978-3-642-33119-0_16","DOI":"10.1007\/978-3-642-33119-0_16"},{"key":"587_CR114","doi-asserted-by":"publisher","unstructured":"Seo, S., Yang, H., Yi, K.: Automatic construction of Hoare proofs from abstract interpretation results. In: Proceedings of APLAS, LNCS, vol. 2895, pp. 230\u2013245. Springer, Berlin (2003). https:\/\/doi.org\/10.1007\/978-3-540-40018-9_16","DOI":"10.1007\/978-3-540-40018-9_16"},{"key":"587_CR115","unstructured":"Sery, O., Fedyukovich, G., Sharygina, N.: Incremental upgrade checking by means of interpolation-based function summaries. In: Proceedings of FMCAD, pp. 114\u2013121. FMCAD Inc., Palo Alto (2012)"},{"key":"587_CR116","doi-asserted-by":"publisher","unstructured":"Sherman, E., Dwyer, M.B.: Structurally defined conditional data-flow static analysis. In: Proceedings of TACAS (2), LNCS, vol. 10806, pp. 249\u2013265. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_15","DOI":"10.1007\/978-3-319-89963-3_15"},{"key":"587_CR117","doi-asserted-by":"publisher","unstructured":"Siddiqui, J.H., Khurshid, S.: Scaling symbolic execution using ranged analysis. In: Leavens, G.T., Dwyer, M.B. (eds.) Proceedings of SPLASH, pp. 523\u2013536. ACM, New York (2012). https:\/\/doi.org\/10.1145\/2384616.2384654","DOI":"10.1145\/2384616.2384654"},{"key":"587_CR118","doi-asserted-by":"publisher","unstructured":"Sokolsky, O., Smolka, S.A.: Incremental model checking in the modal mu-calculus. In: Proceedings of CAV, LNCS, vol. 818, pp. 351\u2013363. Springer, Berlin (1994). https:\/\/doi.org\/10.1007\/3-540-58179-0_67","DOI":"10.1007\/3-540-58179-0_67"},{"key":"587_CR119","doi-asserted-by":"publisher","unstructured":"Staats, M., Pasareanu, C.S.: Parallel symbolic execution for structural test generation. In: Proceedings of ISSTA, pp. 183\u2013194. ACM, New York (2010). https:\/\/doi.org\/10.1145\/1831708.1831732","DOI":"10.1145\/1831708.1831732"},{"key":"587_CR120","doi-asserted-by":"publisher","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 NDSS. Internet Society (2016). https:\/\/doi.org\/10.14722\/ndss.2016.23368","DOI":"10.14722\/ndss.2016.23368"},{"key":"587_CR121","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 MSR. ACM, New York (2014). https:\/\/doi.org\/10.1145\/2597073.2597080","DOI":"10.1145\/2597073.2597080"},{"key":"587_CR122","doi-asserted-by":"publisher","unstructured":"Visser, W., Geldenhuys, J., Dwyer, M.B.: Green: reducing, reusing, and recycling constraints in program analysis. In: Proceedings of FSE, pp. 58:1\u201358:11. ACM, New York (2012). https:\/\/doi.org\/10.1145\/2393596.2393665","DOI":"10.1145\/2393596.2393665"},{"key":"587_CR123","doi-asserted-by":"publisher","unstructured":"Visser, W., P\u0103s\u0103reanu, C.S., Khurshid, S.: Test-input generation with Java PathFinder. In: Proceedings of ISSTA, pp. 97\u2013107. ACM, New York (2004). https:\/\/doi.org\/10.1145\/1007512.1007526","DOI":"10.1145\/1007512.1007526"},{"key":"587_CR124","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, H.H., Leyton-Brown, K.: SATzilla: portfolio-based algorithm selection for SAT. J. Artif. Intell. Res. 32, 565\u2013606 (2008). https:\/\/doi.org\/10.1613\/jair.2490","journal-title":"J. Artif. Intell. Res."},{"key":"587_CR125","doi-asserted-by":"publisher","unstructured":"Xu, Z., Kim, Y., Kim, M., Rothermel, G.: A hybrid directed test-suite augmentation technique. In: Proceedings of ISSRE, pp. 150\u2013159. IEEE (2011). https:\/\/doi.org\/10.1109\/ISSRE.2011.21","DOI":"10.1109\/ISSRE.2011.21"},{"key":"587_CR126","doi-asserted-by":"publisher","unstructured":"Yang, G., Dwyer, M.B., Rothermel, G.: Regression model checking. In: Proceedings of ICSM, pp. 115\u2013124. IEEE (2009). https:\/\/doi.org\/10.1109\/ICSM.2009.5306334","DOI":"10.1109\/ICSM.2009.5306334"},{"key":"587_CR127","doi-asserted-by":"publisher","unstructured":"Yang, G., P\u0103s\u0103reanu, C.S., Khurshid, S.: Memoized symbolic execution. In: Proceedings of ISSTA, pp. 144\u2013154. ACM, New York (2012). https:\/\/doi.org\/10.1145\/2338965.2336771","DOI":"10.1145\/2338965.2336771"},{"key":"587_CR128","doi-asserted-by":"publisher","unstructured":"Yorsh, G., Ball, T., Sagiv, M.: Testing, abstraction, theorem proving: Better together! In: Proceedings of ISSTA, pp. 145\u2013156. ACM, New York (2006). https:\/\/doi.org\/10.1145\/1146238.1146255","DOI":"10.1145\/1146238.1146255"}],"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-020-00587-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-020-00587-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00587-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,30]],"date-time":"2021-07-30T08:08:42Z","timestamp":1627632522000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-020-00587-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4,25]]},"references-count":128,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,6]]}},"alternative-id":["587"],"URL":"https:\/\/doi.org\/10.1007\/s10009-020-00587-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,4,25]]},"assertion":[{"value":"25 April 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}