{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:25:03Z","timestamp":1779074703895,"version":"3.51.4"},"publisher-location":"Cham","reference-count":98,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030613617","type":"print"},{"value":"9783030613624","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,10,29]],"date-time":"2020-10-29T00:00:00Z","timestamp":1603929600000},"content-version":"vor","delay-in-days":302,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The goal of<jats:italic>cooperative<\/jats:italic>verification is to combine verification approaches in such a way that they work together to verify a system model. In particular, cooperative verifiers<jats:italic>provide<\/jats:italic>exchangeable information (verification artifacts)<jats:italic>to<\/jats:italic>other verifiers or<jats:italic>consume<\/jats:italic>such information<jats:italic>from<\/jats:italic>other verifiers with the goal of increasing the overall effectiveness and efficiency of the verification process.<\/jats:p><jats:p>This paper first gives an overview over approaches for leveraging strengths of different techniques, algorithms, and tools in order to increase the power and abilities of the state of the art in software verification. To limit the scope, we restrict our overview to tools and approaches for automatic program analysis. Second, we specifically outline cooperative verification approaches and discuss their employed verification artifacts. Third, we formalize all artifacts in a uniform way, thereby fixing their semantics and providing verifiers with a precise meaning of the exchanged information.<\/jats:p>","DOI":"10.1007\/978-3-030-61362-4_8","type":"book-chapter","created":{"date-parts":[[2020,10,28]],"date-time":"2020-10-28T13:02:36Z","timestamp":1603890156000},"page":"143-167","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":34,"title":["Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4832-7662","authenticated-orcid":false,"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2385-7512","authenticated-orcid":false,"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,10,29]]},"reference":[{"key":"8_CR1","unstructured":"Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley (1995)"},{"key":"8_CR2","unstructured":"Ball, T., Rajamani, S.K.: SLIC: A specification language for interface checking (of C). Technical report MSR-TR-2001-21, Microsoft Research (2002)"},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: Debugging system software via static analysis. In: Proc. POPL, pp. 1\u20133. ACM (2002). https:\/\/doi.org\/10.1145\/503272.503274","DOI":"10.1145\/503272.503274"},{"key":"8_CR4","unstructured":"Ball, T., Bounimova, E., Kumar, R., Levin, V.: SLAM2: Static driver verification with under 4% false alarms. In: Proc. FMCAD, pp. 35\u201342. IEEE (2010)"},{"key":"8_CR5","unstructured":"Baudin, P., Cuoq, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C specification language version 1.15 (2020)"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Beckman, N.E., Nori, A.V., Rajamani, S.K., Simmons, R.J., Tetali, S., Thakur, A.V.: Proofs from tests. IEEE Trans. Softw. Eng. 36(4), 495\u2013508 (2010). https:\/\/doi.org\/10.1109\/TSE.2010.49","DOI":"10.1109\/TSE.2010.49"},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Second competition on software verification (Summary of SV-COMP 2013). In: Proc. TACAS. LNCS, vol. 7795, pp. 594\u2013609. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_43","DOI":"10.1007\/978-3-642-36742-7_43"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Software verification and verifiable witnesses (Report on SV-COMP 2015). In: Proc. TACAS. LNCS, vol. 9035, pp. 401\u2013416. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_31","DOI":"10.1007\/978-3-662-46681-0_31"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating tests from counterexamples. In: Proc. ICSE, pp. 326\u2013335. IEEE (2004). https:\/\/doi.org\/10.1109\/ICSE.2004.1317455","DOI":"10.1109\/ICSE.2004.1317455"},{"key":"8_CR10","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: Proc. SAS. LNCS, vol. 3148, pp. 2\u201318. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-27864-1_2","DOI":"10.1007\/978-3-540-27864-1_2"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M.: Verification-aided debugging: An interactive web-service for exploring error witnesses. In: Proc. CAV (2). LNCS, vol. 9780, pp. 502\u2013509. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_28","DOI":"10.1007\/978-3-319-41540-6_28"},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M.: Strategy selection for software verification based on Boolean features: A simple but effective approach. In: Proc. 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":"8_CR13","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: Exchanging verification results between verifiers. In: Proc. FSE, pp. 326\u2013337. ACM (2016). https:\/\/doi.org\/10.1145\/2950290.2950351","DOI":"10.1145\/2950290.2950351"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Stahlbauer, A.: Witness validation and stepwise testification across software verifiers. In: Proc. FSE, pp. 721\u2013733. ACM (2015). https:\/\/doi.org\/10.1145\/2786805.2786867","DOI":"10.1145\/2786805.2786867"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Lemberger, T., Tautschnig, M.: Tests from witnesses: Execution-based validation of verification results. In: Proc. TAP. LNCS, vol. 10889, pp. 3\u201323. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-92994-1_1","DOI":"10.1007\/978-3-319-92994-1_1"},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Wendler, P.: A unifying view on SMT-based software verification. J. Autom. Reasoning 60(3), 299\u2013335 (2018). https:\/\/doi.org\/10.1007\/s10817-017-9432-6","DOI":"10.1007\/s10817-017-9432-6"},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"Beyer, D., Gulwani, S., Schmidt, D.: Combining model checking and data-flow analysis. In: Handbook of Model Checking, pp. 493\u2013540. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_16","DOI":"10.1007\/978-3-319-10575-8_16"},{"key":"8_CR18","doi-asserted-by":"publisher","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","DOI":"10.1007\/s10009-007-0044-z"},{"key":"8_CR19","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: Proc. FSE. ACM (2012). https:\/\/doi.org\/10.1145\/2393596.2393664","DOI":"10.1145\/2393596.2393664"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Proc. VMCAI. LNCS, vol. 4349, pp. 378\u2013394. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-69738-1_27","DOI":"10.1007\/978-3-540-69738-1_27"},{"key":"8_CR21","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: Proc. PLDI, pp. 300\u2013309. ACM (2007). https:\/\/doi.org\/10.1145\/1250734.1250769","DOI":"10.1145\/1250734.1250769"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Lazy shape analysis. In: Proc. CAV. LNCS, vol. 4144, pp. 532\u2013546. Springer (2006). https:\/\/doi.org\/10.1007\/11817963_48","DOI":"10.1007\/11817963_48"},{"key":"8_CR23","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Program analysis with dynamic precision adjustment. In: Proc. ASE, pp. 29\u201338. IEEE (2008). https:\/\/doi.org\/10.1109\/ASE.2008.13","DOI":"10.1109\/ASE.2008.13"},{"key":"8_CR24","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jakobs, M.C.: CoVeriTest: Cooperative verifier-based testing. In: Proc. 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":"8_CR25","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jakobs, M.C., Lemberger, T., Wehrheim, H.: Reducer-based construction of conditional verifiers. In: Proc. ICSE, pp. 1182\u20131193. ACM (2018). https:\/\/doi.org\/10.1145\/3180155.3180259","DOI":"10.1145\/3180155.3180259"},{"key":"8_CR26","doi-asserted-by":"publisher","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Proc. CAV. LNCS, vol. 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":"8_CR27","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Proc. FMCAD, pp. 189\u2013197. FMCAD (2010)"},{"key":"8_CR28","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lemberger, T.: Conditional testing: Off-the-shelf combination of test-case generators. In: Proc. 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":"8_CR29","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S., Novikov, E., Stahlbauer, A., Wendler, P.: Precision reuse for efficient regression verification. In: Proc. FSE, pp. 389\u2013399. ACM (2013). https:\/\/doi.org\/10.1145\/2491411.2491429","DOI":"10.1145\/2491411.2491429"},{"key":"8_CR30","unstructured":"Beyer, D., Wehrheim, H.: Verification artifacts in cooperative verification: Survey and unifying component framework. arXiv\/CoRR 1905(08505), May 2019. https:\/\/arxiv.org\/abs\/1905.08505"},{"key":"8_CR31","doi-asserted-by":"publisher","unstructured":"Beyer, D., Wendler, P.: Reuse of verification results: Conditional model checking, precision reuse, and verification witnesses. In: Proc. SPIN. LNCS, vol. 7976, pp. 1\u201317. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39176-7_1","DOI":"10.1007\/978-3-642-39176-7_1"},{"key":"8_CR32","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Partial verification and intermediate results as a solution to combine automatic and interactive verification techniques. In: Proc. ISoLA. LNCS, vol. 9952, pp. 874\u2013880. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2","DOI":"10.1007\/978-3-319-47166-2"},{"key":"8_CR33","doi-asserted-by":"publisher","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proc. TACAS. LNCS, vol. 1579, pp. 193\u2013207. Springer (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"key":"8_CR34","doi-asserted-by":"publisher","unstructured":"Casta\u00f1o, R., Braberman, V.A., Garbervetsky, D., Uchitel, S.: Model checker execution reports. In: Proc. ASE, pp. 200\u2013205. IEEE (2017). https:\/\/doi.org\/10.1109\/ASE.2017.8115633","DOI":"10.1109\/ASE.2017.8115633"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Ceri, S., Gottlob, G., Tanca, L.: What you always wanted to know about Datalog (and never dared to ask). IEEE Trans. Knowl. Data Eng. 1(1), 146\u2013166 (1989)","DOI":"10.1109\/69.43410"},{"key":"8_CR36","doi-asserted-by":"publisher","unstructured":"Chalupa, M., Vitovsk\u00e1, M., Strejcek, J.: Symbiotic 5: Boosted instrumentation (competition contribution). In: Proc. TACAS. LNCS, vol. 10806. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_29","DOI":"10.1007\/978-3-319-89963-3_29"},{"key":"8_CR37","doi-asserted-by":"publisher","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Guiding dynamic symbolic execution toward unverified program executions. In: Proc. ICSE, pp. 144\u2013155. ACM (2016). https:\/\/doi.org\/10.1145\/2884781.2884843","DOI":"10.1145\/2884781.2884843"},{"key":"8_CR38","doi-asserted-by":"publisher","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","DOI":"10.1145\/876638.876643"},{"key":"8_CR39","doi-asserted-by":"publisher","unstructured":"Codish, M., Mulkers, A., Bruynooghe, M., de la Banda, M.G., Hermenegildo, M.: Improving abstract interpretations by combining domains. In: Proc. PEPM, pp. 194\u2013205. ACM (1993). https:\/\/doi.org\/10.1145\/154630.154650","DOI":"10.1145\/154630.154650"},{"key":"8_CR40","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Systematic design of program-analysis frameworks. In: Proc. POPL, pp. 269\u2013282. ACM (1979). https:\/\/doi.org\/10.1145\/567752.567778","DOI":"10.1145\/567752.567778"},{"key":"8_CR41","doi-asserted-by":"publisher","unstructured":"Cruanes, S., Hamon, G., Owre, S., Shankar, N.: Tool integration with the Evidential Tool Bus. In: Proc. VMCAI. LNCS, vol. 7737, pp. 275\u2013294. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_18","DOI":"10.1007\/978-3-642-35873-9_18"},{"key":"8_CR42","doi-asserted-by":"crossref","unstructured":"Cruanes, S., Heymans, S., Mason, I., Owre, S., Shankar, N.: The semantics of Datalog for the Evidential Tool Bus. In: Specification, Algebra, and Software, pp. 256\u2013275. Springer (2014)","DOI":"10.1007\/978-3-642-54624-2_13"},{"key":"8_CR43","doi-asserted-by":"publisher","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Proc. SEFM, pp. 233\u2013247. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"8_CR44","doi-asserted-by":"publisher","unstructured":"Czech, M., H\u00fcllermeier, E., Jakobs, M., Wehrheim, H.: Predicting rankings of software verification tools. In: Proc. SWAN, pp. 23\u201326. ACM (2017). https:\/\/doi.org\/10.1145\/3121257.3121262","DOI":"10.1145\/3121257.3121262"},{"key":"8_CR45","doi-asserted-by":"publisher","unstructured":"Czech, M., Jakobs, M., Wehrheim, H.: Just test what you cannot verify! In: Proc. FASE. LNCS, vol. 9033, 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":"8_CR46","doi-asserted-by":"publisher","unstructured":"Daca, P., Gupta, A., Henzinger, T.A.: Abstraction-driven concolic testing. In: Proc. VMCAI. LNCS, vol. 9583, 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":"8_CR47","doi-asserted-by":"publisher","unstructured":"Demyanova, Y., Pani, T., Veith, H., Zuleger, F.: Empirical software metrics for benchmarking of verification tools. In: Proc. CAV. LNCS, vol. 9206, 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":"8_CR48","doi-asserted-by":"publisher","unstructured":"Demyanova, Y., Pani, T., Veith, H., Zuleger, F.: Empirical software metrics for benchmarking of verification tools. Formal Methods Syst. Des. 50(2\u20133), 289\u2013316 (2017). https:\/\/doi.org\/10.1007\/s10703-016-0264-5","DOI":"10.1007\/s10703-016-0264-5"},{"key":"8_CR49","doi-asserted-by":"publisher","unstructured":"Ernst, G., Huisman, M., Mostowski, W., Ulbrich, M.: VerifyThis: Verification competition with a human factor. In: Proc. TACAS. LNCS, vol. 11429, pp. 176\u2013195. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_12","DOI":"10.1007\/978-3-030-17502-3_12"},{"key":"8_CR50","doi-asserted-by":"publisher","unstructured":"Fischer, J., Jhala, R., Majumdar, R.: Joining data flow with predicates. In: Proc. FSE, pp. 227\u2013236. ACM (2005). https:\/\/doi.org\/10.1145\/1081706.1081742","DOI":"10.1145\/1081706.1081742"},{"key":"8_CR51","doi-asserted-by":"publisher","unstructured":"Gerrard, M.J., Dwyer, M.B.: Comprehensive failure characterization. In: Proc. ASE, pp. 365\u2013376. IEEE (2017). https:\/\/doi.org\/10.1109\/ASE.2017.8115649","DOI":"10.1109\/ASE.2017.8115649"},{"key":"8_CR52","doi-asserted-by":"publisher","unstructured":"Gerrard, M.J., Dwyer, M.B.: ALPACA: A large portfolio-based alternating conditional analysis. In: Proc. ICSE, pp. 35\u201338. IEEE (2019). https:\/\/doi.org\/10.1109\/ICSE-Companion.2019.00032","DOI":"10.1109\/ICSE-Companion.2019.00032"},{"key":"8_CR53","doi-asserted-by":"publisher","unstructured":"Godefroid, P., Sen, K.: Combining model checking and testing. In: Handbook of Model Checking, pp. 613\u2013649. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_19","DOI":"10.1007\/978-3-319-10575-8_19"},{"key":"8_CR54","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: Proc. POPL, pp. 43\u201356. ACM (2010). https:\/\/doi.org\/10.1145\/1706299.1706307","DOI":"10.1145\/1706299.1706307"},{"key":"8_CR55","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: Proc. FSE, pp. 117\u2013127. ACM (2006). https:\/\/doi.org\/10.1145\/1181775.1181790","DOI":"10.1145\/1181775.1181790"},{"key":"8_CR56","doi-asserted-by":"publisher","unstructured":"Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: Proc. PLDI, pp. 376\u2013386. ACM (2006). https:\/\/doi.org\/10.1145\/1133981.1134026","DOI":"10.1145\/1133981.1134026"},{"key":"8_CR57","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Albarghouthi, A., Chaki, S., Li, Y., Chechik, M.: Ufo: Verification with interpolants and abstract interpretation (competition contribution). In: Proc. TACAS. LNCS, vol. 7795, pp. 637\u2013640. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_52","DOI":"10.1007\/978-3-642-36742-7_52"},{"key":"8_CR58","doi-asserted-by":"publisher","unstructured":"Harman, M., Hu, L., Hierons, R.M., Wegener, J., Sthamer, H., Baresel, A., Roper, M.: Testability transformation. IEEE Trans. Softw. Eng. 30(1), 3\u201316 (2004). https:\/\/doi.org\/10.1109\/TSE.2004.1265732","DOI":"10.1109\/TSE.2004.1265732"},{"key":"8_CR59","doi-asserted-by":"publisher","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. 44(3) (2012). https:\/\/doi.org\/10.1145\/2187671.2187678","DOI":"10.1145\/2187671.2187678"},{"key":"8_CR60","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":"8_CR61","doi-asserted-by":"publisher","unstructured":"Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: Query-driven program testing. In: Proc. VMCAI. LNCS, vol. 5403, pp. 151\u2013166. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-540-93900-9_15","DOI":"10.1007\/978-3-540-93900-9_15"},{"key":"8_CR62","doi-asserted-by":"publisher","unstructured":"Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: How did you specify your test suite. In: Proc. ASE, pp. 407\u2013416. ACM (2010). https:\/\/doi.org\/10.1145\/1858996.1859084","DOI":"10.1145\/1858996.1859084"},{"key":"8_CR63","doi-asserted-by":"crossref","unstructured":"Huberman, B.A., Lukose, R.M., Hogg, T.: An economics approach to hard computational problems. Science 275(7), 51\u201354 (1997)","DOI":"10.1126\/science.275.5296.51"},{"key":"8_CR64","doi-asserted-by":"publisher","unstructured":"Hutter, F., Hoos, H.H., Leyton-Brown, K.: Sequential model-based optimization for general algorithm configuration. In: Proc. LION. LNCS, vol. 6683, pp. 507\u2013523. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-25566-3_40","DOI":"10.1007\/978-3-642-25566-3_40"},{"key":"8_CR65","doi-asserted-by":"publisher","unstructured":"Jakobs, M.C.: Speed up configurable certificate validation by certificate reduction and partitioning. In: Proc. SEFM. LNCS, vol. 9276, pp. 159\u2013174. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-22969-0_12","DOI":"10.1007\/978-3-319-22969-0_12"},{"key":"8_CR66","doi-asserted-by":"publisher","unstructured":"Jakobs, M.C., Wehrheim, H.: Certification for configurable program analysis. In: Proc. SPIN, pp. 30\u201339. ACM (2014). https:\/\/doi.org\/10.1145\/2632362.2632372","DOI":"10.1145\/2632362.2632372"},{"key":"8_CR67","doi-asserted-by":"publisher","unstructured":"Jakobs, M.: PART$$_{PW}$$ : From partial analysis results to a proof witness. In: Proc. SEFM. LNCS, vol. 10469, pp. 120\u2013135. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-66197-1_8","DOI":"10.1007\/978-3-319-66197-1_8"},{"key":"8_CR68","doi-asserted-by":"publisher","unstructured":"Jakobs, M., Wehrheim, H.: Compact proof witnesses. In: Proc. NFM. LNCS, vol. 10227, pp. 389\u2013403. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_28","DOI":"10.1007\/978-3-319-57288-8_28"},{"key":"8_CR69","doi-asserted-by":"publisher","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: Proc. POPL, pp. 194\u2013206. ACM (1973). https:\/\/doi.org\/10.1145\/512927.512945","DOI":"10.1145\/512927.512945"},{"key":"8_CR70","doi-asserted-by":"publisher","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976). https:\/\/doi.org\/10.1145\/360248.360252","DOI":"10.1145\/360248.360252"},{"key":"8_CR71","doi-asserted-by":"publisher","unstructured":"Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: Proc. CAV. LNCS, vol. 7358, pp. 427\u2013443. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_32","DOI":"10.1007\/978-3-642-31424-7_32"},{"key":"8_CR72","doi-asserted-by":"publisher","unstructured":"Lerner, S., Grove, D., Chambers, C.: Composing data-flow analyses and transformations. In: Proc. POPL, pp. 270\u2013282. ACM (2002). https:\/\/doi.org\/10.1145\/503272.503298","DOI":"10.1145\/503272.503298"},{"key":"8_CR73","doi-asserted-by":"publisher","unstructured":"Leue, S., Befrouei, M.T.: Counterexample explanation by anomaly detection. In: Proc. SPIN. LNCS, vol. 7385, pp. 24\u201342. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31759-0_5","DOI":"10.1007\/978-3-642-31759-0_5"},{"key":"8_CR74","doi-asserted-by":"publisher","unstructured":"Margaria, T., Nagel, R., Steffen, B.: Remote integration and coordination of verification tools in jETI. In: Proc. ECBS, pp. 431\u2013436 (2005). https:\/\/doi.org\/10.1109\/ECBS.2005.59","DOI":"10.1109\/ECBS.2005.59"},{"key":"8_CR75","doi-asserted-by":"publisher","unstructured":"Margaria, T.: Web services-based tool-integration in the ETI platform. Softw. Syst. Modeling 4(2), 141\u2013156 (2005). https:\/\/doi.org\/10.1007\/s10270-004-0072-z","DOI":"10.1007\/s10270-004-0072-z"},{"key":"8_CR76","doi-asserted-by":"publisher","unstructured":"Margaria, T., Nagel, R., Steffen, B.: jETI: A tool for remote tool integration. In: Proc. TACAS. LNCS, vol. 3440, pp. 557\u2013562. Springer (2005). https:\/\/doi.org\/10.1007\/978-3-540-31980-1_38","DOI":"10.1007\/978-3-540-31980-1_38"},{"key":"8_CR77","doi-asserted-by":"publisher","unstructured":"M\u00fcller, P., Peringer, P., Vojnar, T.: Predator hunting party (competition contribution). In: Proc. TACAS. LNCS, vol. 9035, pp. 443\u2013446. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_40","DOI":"10.1007\/978-3-662-46681-0_40"},{"key":"8_CR78","doi-asserted-by":"crossref","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: Cil: Intermediate language and tools for analysis and transformation of C programs. In: Proc. CC. LNCS, vol. 2304, pp. 213\u2013228. Springer (2002)","DOI":"10.1007\/3-540-45937-5_16"},{"key":"8_CR79","doi-asserted-by":"publisher","unstructured":"Necula, G.C., McPeak, S., Weimer, W.: CCured: Type-safe retrofitting of legacy code. In: Proc. POPL, pp. 128\u2013139. ACM (2002). https:\/\/doi.org\/10.1145\/503272.503286","DOI":"10.1145\/503272.503286"},{"key":"8_CR80","doi-asserted-by":"publisher","unstructured":"Nori, A.V., Rajamani, S.K., Tetali, S., Thakur, A.V.: The Yogi Project: Software property checking via static analysis and testing. In: Proc. TACAS. LNCS, vol. 5505, 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"},{"key":"8_CR81","doi-asserted-by":"publisher","unstructured":"Novikov, E., Zakharov, I.S.: Towards automated static verification of GNU C programs. In: Proc. PSI. LNCS, vol. 10742, pp. 402\u2013416. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-74313-4_30","DOI":"10.1007\/978-3-319-74313-4_30"},{"key":"8_CR82","doi-asserted-by":"publisher","unstructured":"Pauck, F., Bodden, E., Wehrheim, H.: Do Android taint-analysis tools keep their promises? In: Proc. ESEC\/FSE, pp. 331\u2013341. ACM (2018). https:\/\/doi.org\/10.1145\/3236024.3236029","DOI":"10.1145\/3236024.3236029"},{"key":"8_CR83","doi-asserted-by":"publisher","unstructured":"Pauck, F., Wehrheim, H.: Together strong: Cooperative Android App analysis. In: Proc. ESEC\/FSE, pp. 374\u2013384. ACM (2019). https:\/\/doi.org\/10.1145\/3338906.3338915","DOI":"10.1145\/3338906.3338915"},{"key":"8_CR84","doi-asserted-by":"publisher","unstructured":"Piterman, N., Pnueli, A.: Temporal logic and fair discrete systems. In: Handbook of Model Checking, pp. 27\u201373. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_2","DOI":"10.1007\/978-3-319-10575-8_2"},{"key":"8_CR85","doi-asserted-by":"publisher","unstructured":"Rice, J.R.: The algorithm selection problem. Adv. Comput. 15, 65\u2013118 (1976). https:\/\/doi.org\/10.1016\/S0065-2458(08)60520-3","DOI":"10.1016\/S0065-2458(08)60520-3"},{"key":"8_CR86","doi-asserted-by":"publisher","unstructured":"Rothenberg, B., Dietsch, D., Heizmann, M.: Incremental verification using trace abstraction. In: Proc. SAS. LNCS, vol. 11002, pp. 364\u2013382. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-99725-4_22","DOI":"10.1007\/978-3-319-99725-4_22"},{"key":"8_CR87","doi-asserted-by":"publisher","unstructured":"Ser\u00fd, O.: Enhanced property specification and verification in Blast. In: Proc. FASE. LNCS, vol. 5503, pp. 456\u2013469. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-00593-0_32","DOI":"10.1007\/978-3-642-00593-0_32"},{"key":"8_CR88","doi-asserted-by":"publisher","unstructured":"Shankar, N.: Combining model checking and deduction. In: Handbook of Model Checking, pp. 651\u2013684. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_20","DOI":"10.1007\/978-3-319-10575-8_20"},{"key":"8_CR89","doi-asserted-by":"publisher","unstructured":"Sherman, E., Dwyer, M.B.: Structurally defined conditional data-flow static analysis. In: Proc. TACAS (2). LNCS, vol. 10806, pp. 249\u2013265. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_15","DOI":"10.1007\/978-3-319-89963-3_15"},{"key":"8_CR90","doi-asserted-by":"publisher","unstructured":"Steffen, B.: The physics of software tools: SWOT analysis and vision. Int. J. Softw. Tools Technol. Transf. 19(1), 1\u20137 (2017). https:\/\/doi.org\/10.1007\/s10009-016-0446-x","DOI":"10.1007\/s10009-016-0446-x"},{"key":"8_CR91","doi-asserted-by":"publisher","unstructured":"Steffen, B., Margaria, T., Braun, V.: The Electronic Tool Integration platform: Concepts and design. STTT 1(1\u20132), 9\u201330 (1997). https:\/\/doi.org\/10.1007\/s100090050003","DOI":"10.1007\/s100090050003"},{"key":"8_CR92","doi-asserted-by":"publisher","unstructured":"Torsney-Weir, T., Saad, A., M\u00f6ller, T., Hege, H., Weber, B., Verbavatz, J.: Tuner: Principled parameter finding for image segmentation algorithms using visual response surface exploration. IEEE Trans. Vis. Comput. Graph. 17(12), 1892\u20131901 (2011). https:\/\/doi.org\/10.1109\/TVCG.2011.248","DOI":"10.1109\/TVCG.2011.248"},{"key":"8_CR93","doi-asserted-by":"publisher","unstructured":"Tulsian, V., Kanade, A., Kumar, R., Lal, A., Nori, A.V.: MUX: Algorithm selection for software model checkers. In: Proc. MSR. ACM (2014). https:\/\/doi.org\/10.1145\/2597073.2597080","DOI":"10.1145\/2597073.2597080"},{"key":"8_CR94","unstructured":"Turing, A.: Checking a large routine. In: Report on a Conference on High Speed Automatic Calculating Machines, pp. 67\u201369. Cambridge Univ. Math. Lab. (1949)"},{"key":"8_CR95","doi-asserted-by":"publisher","unstructured":"Visser, W., Geldenhuys, J., Dwyer, M.B.: Green: Reducing, reusing, and recycling constraints in program analysis. In: Proc. FSE, pp. 58:1\u201358:11. ACM (2012). https:\/\/doi.org\/10.1145\/2393596.2393665","DOI":"10.1145\/2393596.2393665"},{"key":"8_CR96","doi-asserted-by":"publisher","unstructured":"Visser, W., P\u0103s\u0103reanu, C.S., Khurshid, S.: Test-input generation with Java PathFinder. In: Proc. ISSTA, pp. 97\u2013107. ACM (2004). https:\/\/doi.org\/10.1145\/1007512.1007526","DOI":"10.1145\/1007512.1007526"},{"key":"8_CR97","doi-asserted-by":"publisher","unstructured":"Wendler, P.: CPAchecker with sequential combination of explicit-state analysis and predicate analysis (competition contribution). In: Proc. TACAS. LNCS, vol. 7795, pp. 613\u2013615. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_45","DOI":"10.1007\/978-3-642-36742-7_45"},{"key":"8_CR98","doi-asserted-by":"publisher","unstructured":"Xie, T., Zhang, L., Xiao, X., Xiong, Y., Hao, D.: Cooperative software testing and analysis: Advances and challenges. J. Comput. Sci. Technol. 29(4), 713\u2013723 (2014). https:\/\/doi.org\/10.1007\/s11390-014-1461-6","DOI":"10.1007\/s11390-014-1461-6"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-61362-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,25]],"date-time":"2022-11-25T04:50:19Z","timestamp":1669351819000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-61362-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030613617","9783030613624"],"references-count":98,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-61362-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"29 October 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/isola-conference.org\/isola2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}