{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,25]],"date-time":"2026-08-25T22:34:46Z","timestamp":1787697286029,"version":"build-2784847793"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2024,12,24]],"date-time":"2024-12-24T00:00:00Z","timestamp":1734998400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,12,24]],"date-time":"2024-12-24T00:00:00Z","timestamp":1734998400000},"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":["SN COMPUT. SCI."],"DOI":"10.1007\/s42979-024-03482-0","type":"journal-article","created":{"date-parts":[[2024,12,24]],"date-time":"2024-12-24T10:29:13Z","timestamp":1735036153000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Seeding Contradiction: a Fast Method for Generating Full-Coverage Test Suites"],"prefix":"10.1007","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3531-4045","authenticated-orcid":false,"given":"Li","family":"Huang","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bertrand","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Manuel","family":"Oriol","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,12,24]]},"reference":[{"key":"3482_CR1","doi-asserted-by":"crossref","unstructured":"Pacheco C, Ernst MD. Randoop: feedback-directed random testing for java. In: Companion to the 22nd ACM SIGPLAN Conference on Object-oriented Programming Systems and Applications Companion 2007;815\u20136.","DOI":"10.1145\/1297846.1297902"},{"key":"3482_CR2","doi-asserted-by":"crossref","unstructured":"Tillmann N, De Halleux J. Pex-White Box Test Generation for. Net. In: International Conference on Tests and Proofs (TAP). 2008;134\u201353. Springer","DOI":"10.1007\/978-3-540-79124-9_10"},{"key":"3482_CR3","unstructured":"AutoTest. https:\/\/www.eiffel.org\/doc\/eiffelstudio\/Using_AutoTest"},{"issue":"4","key":"3482_CR4","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/566171.566191","volume":"27","author":"C Boyapati","year":"2002","unstructured":"Boyapati C, Khurshid S, Marinov D. Korat: Automated testing based on java predicates. ACM SIGSOFT Software Engineering Notes. 2002;27(4):123\u201333.","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"3482_CR5","doi-asserted-by":"crossref","unstructured":"Ahrendt W, Beckert B, Bruns D, Bubel R, Gladisch C, Grebing S, H\u00e4hnle R, Hentschel M, Herda M, Klebanov V. The key platform for verification and analysis of java programs. 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers In: Verified Software: Theories, Tools and Experiments.6 2014;55\u201371. . Springer","DOI":"10.1007\/978-3-319-12154-3_4"},{"key":"3482_CR6","doi-asserted-by":"crossref","unstructured":"Sen K, Agha G. Cute and jcute: Concolic unit testing and explicit path model-checking tools: (tool paper). In: Computer Aided Verification: 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006. Proceedings 18, 2006;419\u2013423 Springer","DOI":"10.1007\/11817963_38"},{"key":"3482_CR7","doi-asserted-by":"crossref","unstructured":"Nilizadeh A, Calvo M, Leavens GT, Cok DR. Generating Counterexamples in the Form of Unit Tests from Hoare-style Verification Attempts. In: International Conference on Formal Methods in Software Engineering (FormaliSE), 2022;124\u2013128. IEEE","DOI":"10.1145\/3524482.3527656"},{"key":"3482_CR8","doi-asserted-by":"crossref","unstructured":"Huang L, Meyer B. A Failed Proof Can Yield a Useful Test. arXiv:2208.09873 2022","DOI":"10.1002\/stvr.1859"},{"key":"3482_CR9","doi-asserted-by":"crossref","unstructured":"Huang L, Meyer B, Oriol M. Improving Counterexample Quality from Failed Program Verification. In: International Symposium on Software Reliability Engineering Workshops (ISSREW), 2022;268\u2013273. IEEE","DOI":"10.1109\/ISSREW55968.2022.00078"},{"key":"3482_CR10","doi-asserted-by":"crossref","unstructured":"Tschannen J, Furia CA, Nordio M, Polikarpova N. AutoProof: Auto-active Functional Verification of Object-Oriented Programs. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2015;566\u2013580 . Springer","DOI":"10.1007\/978-3-662-46681-0_53"},{"key":"3482_CR11","unstructured":"AutoProof. http:\/\/autoproof.sit.org\/"},{"key":"3482_CR12","unstructured":"Meyer B. Object-Oriented Software Construction, second edition. Prentice Hall 1997"},{"key":"3482_CR13","unstructured":"Leino KRM, R\u00fcmmer P. The Boogie 2 Type System: Design and Verification Condition Generation. https:\/\/citeseerx.ist.psu.edu\/viewdoc\/summary?doi=10.1.1.146.4277"},{"key":"3482_CR14","doi-asserted-by":"crossref","unstructured":"Barnett M, Chang B-YE, DeLine R, Jacobs B, Leino KRM. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: Int. Symposium on Formal Methods for Components and Objects, 2005;364\u2013387 . Springer","DOI":"10.1007\/11804192_17"},{"key":"3482_CR15","doi-asserted-by":"crossref","unstructured":"De Moura L, Bj\u00f8rner N. Z3: An Efficient SMT Solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008;337\u2013340. Springer","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"3482_CR16","unstructured":"Leino KRM. Program Proofs. MIT Press 2023"},{"issue":"6","key":"3482_CR17","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1145\/318774.318939","volume":"24","author":"A Gargantini","year":"1999","unstructured":"Gargantini A, Heitmeyer C. Using model checking to generate tests from requirements specifications. ACM SIGSOFT Software Engineering Notes. 1999;24(6):146\u201362.","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"3482_CR18","doi-asserted-by":"crossref","unstructured":"Rayadurgam S. Heimdahl MPE. Coverage based test-case generation using model checkers. In: Proceedings. Eighth Annual IEEE International Conference and Workshop On the Engineering of Computer-Based Systems-ECBS 2001, 2001;83\u201391. IEEE","DOI":"10.1109\/ECBS.2001.922409"},{"key":"3482_CR19","unstructured":"Meyer B. Loop unrolling (for test coverage): formal definition. arXiv 2024"},{"key":"3482_CR20","doi-asserted-by":"publisher","first-page":"847","DOI":"10.1007\/s10009-020-00572-1","volume":"23","author":"M-C Jakobs","year":"2021","unstructured":"Jakobs M-C. Coveritest: interleaving value and predicate analysis for test-case generation. International journal on software tools for technology transfer. 2021;23:847\u201351.","journal-title":"International journal on software tools for technology transfer"},{"key":"3482_CR21","doi-asserted-by":"crossref","unstructured":"Beyer D, Keremoglu ME. Cpachecker: A tool for configurable software verification. In: Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings 23, 2011;184\u2013190. Springer","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"3482_CR22","doi-asserted-by":"crossref","unstructured":"Ciupa I, Leitner A, Oriol M, Meyer B. ARTOO: Adaptive Random Testing for Object-Oriented Software. In: International Conference on Software Engineering (ICSE), 2008;71\u201380","DOI":"10.1145\/1368088.1368099"},{"key":"3482_CR23","doi-asserted-by":"crossref","unstructured":"Weide BW, Sitaraman M, Harton HK, Adcock B, Bucci P, Bronish D, Heym WD, Kirschenbaum J, Frazier D. Incremental Benchmarks for Software Verification Tools and Techniques. In: Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), 2008;84\u201398. Springer","DOI":"10.1007\/978-3-540-87873-5_10"},{"key":"3482_CR24","doi-asserted-by":"crossref","unstructured":"Bormer T. Brockschmidt M. Distefano D. The COST IC0701 Verification Competition. In: International Conference on Formal Verification of Object-Oriented Software (FoVeOO), 2011;3\u201321. Springer","DOI":"10.1007\/978-3-642-31762-0_2"},{"key":"3482_CR25","doi-asserted-by":"crossref","unstructured":"Klebanov V. M\u00fcller P. The 1st Verified Software Competition: Experience Report. In: International Symposium on Formal Methods (FM), 2011;154\u2013168. Springer","DOI":"10.1007\/978-3-642-21437-0_14"},{"key":"3482_CR26","doi-asserted-by":"crossref","unstructured":"Orso A. Hsu H-Y. MINTS: A General Framework and Tool for Supporting Test-suite Minimization. In: International Conference on Software Engineering (ICSE), 2009;419\u2013429","DOI":"10.1109\/ICSE.2009.5070541"},{"key":"3482_CR27","doi-asserted-by":"crossref","unstructured":"Sen K, Marinov D, Agha G CUTE: a Concolic Unit Testing Engine for C. In: The ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC-FSE), 2005;213\u2013223","DOI":"10.21236\/ADA482657"},{"key":"3482_CR28","doi-asserted-by":"crossref","unstructured":"Huang L, Meyer B, Oriol M. Seeding contradiction: a fast method for generating full-coverage test suites. In: IFIP International Conference on Testing Software and Systems, 2023;52\u201370. Springer","DOI":"10.1007\/978-3-031-43240-8_4"},{"key":"3482_CR29","doi-asserted-by":"crossref","unstructured":"Nilizadeh A, Calvo M, Leavens GT, Le X-BD. More Reliable Test Suites for Dynamic APR by Using Counterexamples. In: International Symposium on Software Reliability Engineering (ISSRE), 2021;208\u2013219. IEEE","DOI":"10.1109\/ISSRE52982.2021.00032"},{"key":"3482_CR30","doi-asserted-by":"crossref","unstructured":"Angeletti D, Giunchiglia E, Narizzano M, Palma G, Puddu A, Sabina S. Improving the Automatic Test Generation Process for Coverage Analysis Using CBMC. In: International RCRA Workshop 2009","DOI":"10.1007\/978-3-642-04772-5_38"},{"key":"3482_CR31","doi-asserted-by":"crossref","unstructured":"Angeletti D, Giunchiglia E, Narizzano M, Puddu A, Sabina S. Automatic Test Generation for Coverage Analysis Using CBMC. In: International Conference on Computer Aided Systems Theory (EUROCAST), 2009;287\u2013294. Springer","DOI":"10.1007\/978-3-642-04772-5_38"},{"key":"3482_CR32","doi-asserted-by":"crossref","unstructured":"Kroening D, Tautschnig M. CBMC\u2013C Bounded Model Checker: (Competition Contribution). In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2014;389\u2013391. Springer","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"3482_CR33","unstructured":"Brenguier R, Cordeiro L, Kroening D, Schrammel P. JBMC: A Bounded Model Checking Tool for Java Bytecode. arXiv:2302.02381 2023"},{"key":"3482_CR34","unstructured":"Cadar C, Dunbar D, Engler DR. KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. In: USENIX Symposium on Operating Systems Design and Implementation (OSDI), vol. 8, 2008;209\u2013224"},{"key":"3482_CR35","doi-asserted-by":"crossref","unstructured":"Williams N. Towards Exhaustive Branch Coverage with PathCrawler. In: Int. Conference on Automation of Software Tests (AST), 2021;117\u2013120. IEEE","DOI":"10.1109\/AST52587.2021.00022"},{"key":"3482_CR36","doi-asserted-by":"crossref","unstructured":"Fedchin A, Dean T, Foster JS, Mercer E, Rakamaric Z, Reger G, Rungta N, Salkeld R, Wagner L, Waldrip C. A Toolkit for Automated Testing of Dafny 2023","DOI":"10.1007\/978-3-031-33170-1_24"}],"container-title":["SN Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s42979-024-03482-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s42979-024-03482-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s42979-024-03482-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,24]],"date-time":"2024-12-24T11:15:00Z","timestamp":1735038900000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s42979-024-03482-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,24]]},"references-count":36,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2025,1]]}},"alternative-id":["3482"],"URL":"https:\/\/doi.org\/10.1007\/s42979-024-03482-0","relation":{},"ISSN":["2661-8907"],"issn-type":[{"value":"2661-8907","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,12,24]]},"assertion":[{"value":"19 March 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 October 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 December 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"On behalf of all authors, the corresponding author declares that there is no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"41"}}