{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:19:34Z","timestamp":1740107974709,"version":"3.37.3"},"reference-count":10,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2020,7,6]],"date-time":"2020-07-06T00:00:00Z","timestamp":1593993600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,7,6]],"date-time":"2020-07-06T00:00:00Z","timestamp":1593993600000},"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,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Verification techniques are well-suited for automatic test-case generation. They basically need to check the reachability of every test goal and generate test cases for all reachable goals. This is also the basic idea of our <jats:sc>CoVeriTest<\/jats:sc>\u00a0submission. However, the set of test goals is not fixed in <jats:sc>CoVeriTest<\/jats:sc>\u00a0, instead we can configure the set of test goals. For Test-Comp\u201919, we support the set of all ___ calls as well as the set of all branches. Thus, we can deal with the two test specifications considered in Test-Comp\u201919. Since the tasks in Test-Comp are diverse and verification techniques have different strengths and weaknesses, we also do not stick to a single verification technique, but use a hybrid approach that combines multiple techniques. More concrete, <jats:sc>CoVeriTest<\/jats:sc>\u00a0interleaves different verification techniques and allows to configure the cooperation (i.e., information exchange and time limits). To choose from a large set of verification techniques, <jats:sc>CoVeriTest<\/jats:sc>\u00a0is integrated into the analysis framework <jats:sc>CPAchecker<\/jats:sc>. For the competition, we interleave <jats:sc>CPAchecker<\/jats:sc>\u2019s value and predicate analysis and let both analyses resume their analysis performed in the previous iteration.<\/jats:p>","DOI":"10.1007\/s10009-020-00572-1","type":"journal-article","created":{"date-parts":[[2020,7,6]],"date-time":"2020-07-06T10:02:52Z","timestamp":1594029772000},"page":"847-851","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["CoVeriTest: interleaving value and predicate analysis for test-case generation"],"prefix":"10.1007","volume":"23","author":[{"given":"Marie-Christine","family":"Jakobs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,7,6]]},"reference":[{"key":"572_CR1","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":"572_CR2","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 (2012). https:\/\/doi.org\/10.1145\/2393596.2393664","DOI":"10.1145\/2393596.2393664"},{"key":"572_CR3","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Configurable software verification: concretizing the convergence of model checking and program analysis. In: Proceedings of CAV, LNCS 4590, pp. 504\u2013518. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_51","DOI":"10.1007\/978-3-540-73368-3_51"},{"key":"572_CR4","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jakobs, M.: CoVeriTest: cooperative verifier-based testing. In: Proceedings of FASE, LNCS 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":"572_CR5","doi-asserted-by":"publisher","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Proceedings of CAV, LNCS 6806, 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":"572_CR6","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Proceedings of FMCAD, pp. 189\u2013197. FMCAD (2010). http:\/\/ieeexplore.ieee.org\/document\/5770949\/"},{"key":"572_CR7","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 7793, pp. 146\u2013162. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-37057-1_11","DOI":"10.1007\/978-3-642-37057-1_11"},{"key":"572_CR8","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Proceedings of TACAS, LNCS 7795, pp. 93\u2013107. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7","DOI":"10.1007\/978-3-642-36742-7_7"},{"issue":"5","key":"572_CR9","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003). https:\/\/doi.org\/10.1145\/876638.876643","journal-title":"J. ACM"},{"key":"572_CR10","doi-asserted-by":"publisher","unstructured":"Karpenkov, E.G., Friedberger, K., Beyer, D.: JavaSMT: a unified\u00a0interface for SMT solvers in Java. In: Proceedings of VSTTE, LNCS 9971, pp. 139\u2013148. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-48869-1_11","DOI":"10.1007\/978-3-319-48869-1_11"}],"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-00572-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-020-00572-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-020-00572-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,26]],"date-time":"2021-12-26T12:03:02Z","timestamp":1640520182000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-020-00572-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,6]]},"references-count":10,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["572"],"URL":"https:\/\/doi.org\/10.1007\/s10009-020-00572-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2020,7,6]]},"assertion":[{"value":"6 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}