{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T16:07:13Z","timestamp":1743005233428,"version":"3.40.3"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031720437"},{"type":"electronic","value":"9783031720444"}],"license":[{"start":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T00:00:00Z","timestamp":1725926400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T00:00:00Z","timestamp":1725926400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-72044-4_3","type":"book-chapter","created":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T16:02:41Z","timestamp":1725897761000},"page":"45-64","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Refining CEGAR-Based Test-Case Generation with\u00a0Feasibility Annotations"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-7716-3898","authenticated-orcid":false,"given":"Max","family":"Barth","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5890-4673","authenticated-orcid":false,"given":"Marie-Christine","family":"Jakobs","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,10]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","unstructured":"Agrawal, H.: Dominators, super blocks, and program coverage. In: POPL, pp. 25\u201334. ACM (1994). https:\/\/doi.org\/10.1145\/174675.175935","DOI":"10.1145\/174675.175935"},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Alshmrany, K., Aldughaim, M., Bhayat, A., Cordeiro, L.: FuSeBMC v4: Improving code coverage with smart seeds via BMC, fuzzing and static analysis. FAC (2024). https:\/\/doi.org\/10.1145\/3665337","DOI":"10.1145\/3665337"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-030-79379-1_6","volume-title":"Tests and Proofs","author":"KM 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: Loulergue, F., Wotawa, F. (eds.) TAP 2021. LNCS, vol. 12740, pp. 85\u2013105. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79379-1_6"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Barth, M., Jakobs, M.: Replication package for paper \u201cRefining CEGAR-based test-case generation with feasibility annotations\u201d (2024). https:\/\/doi.org\/10.5281\/zenodo.11641893","DOI":"10.5281\/zenodo.11641893"},{"key":"3_CR5","doi-asserted-by":"publisher","unstructured":"Barth, M., Jakobs, M.C.: Test-case generation with automata-based software model checking. In: Neele, T., Wijs A. (eds.) SPIN 2024. LNCS, vol. 14624, pp. 1\u201320. Spinger, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-66149-5_14","DOI":"10.1007\/978-3-031-66149-5_14"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-031-30826-0_17","volume-title":"Fundamental Approaches to Software Engineering","author":"D Beyer","year":"2023","unstructured":"Beyer, D.: Software testing: 5th comparative evaluation: Test-Comp 2023. In: Lambers, L., Uchitel, S. (eds.) FASE 2023. LNCS, vol. 13991, pp. 309\u2013323. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30826-0_17"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"Beyer, D., Chlipala, A., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating tests from counterexamples. In: ICSE, pp. 326\u2013335. IEEE (2004). https:\/\/doi.org\/10.1109\/ICSE.2004.1317455","DOI":"10.1109\/ICSE.2004.1317455"},{"key":"3_CR8","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., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 493\u2013540. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_16"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-030-16722-6_23","volume-title":"Fundamental Approaches to Software Engineering","author":"D Beyer","year":"2019","unstructured":"Beyer, D., Jakobs, M.-C.: CoVeriTest: Cooperative verifier-based testing. In: H\u00e4hnle, R., van der Aalst, W. (eds.) FASE 2019. LNCS, vol. 11424, pp. 389\u2013408. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-16722-6_23"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-030-31784-3_11","volume-title":"Automated Technology for Verification and Analysis","author":"D Beyer","year":"2019","unstructured":"Beyer, D., Lemberger, T.: Conditional testing - off-the-shelf combination of test-case generators. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 189\u2013208. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_11"},{"key":"3_CR11","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lemberger, T.: TestCov: Robust test-suite execution and coverage measurement. In: ASE, pp. 1074\u20131077. IEEE (2019).https:\/\/doi.org\/10.1109\/ASE.2019.00105","DOI":"10.1109\/ASE.2019.00105"},{"issue":"1","key":"3_CR12","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. STTT 21(1), 1\u201329 (2019). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","journal-title":"STTT"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"Busse, F., Nowack, M., Cadar, C.: Running symbolic execution forever. In: ISSTA, pp. 63\u201374. ACM (2020) https:\/\/doi.org\/10.1145\/3395363.3397360","DOI":"10.1145\/3395363.3397360"},{"key":"3_CR14","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, pp. 209\u2013224. USENIX Association (2008). http:\/\/www.usenix.org\/events\/osdi08\/tech\/full_papers\/cadar\/cadar.pdf"},{"issue":"5","key":"3_CR15","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1109\/TSE.1987.233196","volume":"13","author":"T Chusho","year":"1987","unstructured":"Chusho, T.: Test data selection and quality estimation based on the concept of esssential branches for path testing. IEEE TSE 13(5), 509\u2013517 (1987). https:\/\/doi.org\/10.1109\/TSE.1987.233196","journal-title":"IEEE TSE"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_15"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/978-3-031-33170-1_24","volume-title":"NASA Formal Methods","author":"A Fedchin","year":"2023","unstructured":"Fedchin, A., et al.: A toolkit for automated testing of Dafny. In: Rozier, K.Y., Chaudhuri, S. (eds.) NFM 2023. LNCS, vol. 13903, pp. 397\u2013413. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-33170-1_24"},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Fraser, G., Arcuri, A.: Evolutionary generation of whole test suites. In: QSIC, pp. 31\u201340. IEEE (2011). https:\/\/doi.org\/10.1109\/QSIC.2011.19","DOI":"10.1109\/QSIC.2011.19"},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. In: PLDI, pp. 213\u2013223. ACM (2005). https:\/\/doi.org\/10.1145\/1065010.1065036","DOI":"10.1145\/1065010.1065036"},{"key":"3_CR20","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. In: NDSS. The Internet Society (2008). https:\/\/www.ndss-symposium.org\/ndss2008\/automated-whitebox-fuzz-testing\/"},{"key":"3_CR21","doi-asserted-by":"publisher","unstructured":"G\u00fcdemann, M., Schrammel, P.: BlueCov: Integrating test coverage and model checking with JBMC. In: SAC, pp. 1695\u20131697. ACM (2023). https:\/\/doi.org\/10.1145\/3555776.3577829","DOI":"10.1145\/3555776.3577829"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-540-93900-9_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Holzer","year":"2008","unstructured":"Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: Query-driven program testing. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 151\u2013166. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-93900-9_15"},{"key":"3_CR23","doi-asserted-by":"publisher","unstructured":"Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: How did you specify your test suite. In: ASE, pp. 407\u2013416. ACM (2010).https:\/\/doi.org\/10.1145\/1858996.1859084","DOI":"10.1145\/1858996.1859084"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-540-31848-4_8","volume-title":"Formal Approaches to Software Testing","author":"HS Hong","year":"2005","unstructured":"Hong, H.S., Ural, H.: Using model checking for reducing the cost of test generation. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 110\u2013124. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31848-4_8"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1007\/978-3-642-31424-7_61","volume-title":"Computer Aided Verification","author":"J Jaffar","year":"2012","unstructured":"Jaffar, J., Murali, V., Navas, J.A., Santosa, A.E.: TRACER: A symbolic execution tool for verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 758\u2013766. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_61"},{"key":"3_CR26","doi-asserted-by":"publisher","unstructured":"Jia, X., Ghezzi, C., Ying, S.: Enhancing reuse of constraint solutions to improve symbolic execution. In: ISSTA, pp. 177\u2013187. ACM (2015). https:\/\/doi.org\/10.1145\/2771783.2771806","DOI":"10.1145\/2771783.2771806"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-031-57256-2_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Jon\u00e1s","year":"2024","unstructured":"Jon\u00e1s, M., Strejcek, J., Trt\u00edk, M., Urban, L.: Gray-box fuzzing via gradient descent and Boolean expression coverage. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) TACAS 2024. LNCS, vol. 14572, pp. 90\u2013109. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_5"},{"issue":"6","key":"3_CR28","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. STTT 23(6), 871\u2013873 (2021). https:\/\/doi.org\/10.1007\/s10009-020-00568-x","journal-title":"STTT"},{"key":"3_CR29","doi-asserted-by":"publisher","unstructured":"Lemieux, C., Sen, K.: FairFuzz: A targeted mutation strategy for increasing greybox fuzz testing coverage. In: ASE, pp. 475\u2013485. ACM (2018).https:\/\/doi.org\/10.1145\/3238147.3238176","DOI":"10.1145\/3238147.3238176"},{"issue":"11","key":"3_CR30","doi-asserted-by":"publisher","first-page":"2312","DOI":"10.1109\/TSE.2019.2946563","volume":"47","author":"VJM Man\u00e8s","year":"2021","unstructured":"Man\u00e8s, V.J.M., et al.: The art, science, and engineering of fuzzing: A survey. IEEE TSE 47(11), 2312\u20132331 (2021). https:\/\/doi.org\/10.1109\/TSE.2019.2946563","journal-title":"IEEE TSE"},{"issue":"11","key":"3_CR31","doi-asserted-by":"publisher","first-page":"974","DOI":"10.1109\/TSE.2003.1245299","volume":"29","author":"M Marr\u00e9","year":"2003","unstructured":"Marr\u00e9, M., Bertolino, A.: Using spanning sets for coverage testing. IEEE TSE 29(11), 974\u2013984 (2003). https:\/\/doi.org\/10.1109\/TSE.2003.1245299","journal-title":"IEEE TSE"},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-14295-6_10","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2010","unstructured":"McMillan, K.L.: Lazy annotation for program testing and verification. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 104\u2013118. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_10"},{"issue":"6","key":"3_CR33","doi-asserted-by":"publisher","first-page":"853","DOI":"10.1007\/s10009-020-00574-z","volume":"23","author":"S Ruland","year":"2021","unstructured":"Ruland, S., Lochau, M., Fehse, O., Sch\u00fcrr, A.: CPA\/Tiger-MGP: Test-goal set partitioning for efficient multi-goal test-suite generation. STTT 23(6), 853\u2013856 (2021). https:\/\/doi.org\/10.1007\/s10009-020-00574-z","journal-title":"STTT"},{"key":"3_CR34","doi-asserted-by":"publisher","unstructured":"Visser, W., Geldenhuys, J., Dwyer, M.B.: Green: Reducing, reusing and recycling constraints in program analysis. In: FSE, p.\u00a058. ACM (2012).https:\/\/doi.org\/10.1145\/2393596.2393665","DOI":"10.1145\/2393596.2393665"},{"key":"3_CR35","doi-asserted-by":"publisher","unstructured":"Yang, G., Pasareanu, C.S., Khurshid, S.: Memoized symbolic execution. In: ISSTA, pp. 144\u2013154. ACM (2012)https:\/\/doi.org\/10.1145\/2338965.2336771","DOI":"10.1145\/2338965.2336771"},{"issue":"2","key":"3_CR36","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1002\/STV.430","volume":"22","author":"S Yoo","year":"2012","unstructured":"Yoo, S., Harman, M.: Regression testing minimization, selection and prioritization: A survey. STVR 22(2), 67\u2013120 (2012). https:\/\/doi.org\/10.1002\/STV.430","journal-title":"STVR"},{"key":"3_CR37","doi-asserted-by":"publisher","unstructured":"Zlatkin, I., Fedyukovich, G.: Maximizing branch coverage with constrained horn clauses. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13244, pp. 254\u2013272. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_14","DOI":"10.1007\/978-3-030-99527-0_14"}],"container-title":["Lecture Notes in Computer Science","Tests and Proofs"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-72044-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T16:05:06Z","timestamp":1725897906000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-72044-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,10]]},"ISBN":["9783031720437","9783031720444"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-72044-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,9,10]]},"assertion":[{"value":"10 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"All experimental data, all used software as well as the test tasks are publicly available in our supplementary artifact\u00a0[].","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Data-Availability Statement"}},{"value":"TAP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tests and Proofs","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tap2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}