{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,28]],"date-time":"2025-08-28T12:51:27Z","timestamp":1756385487765,"version":"3.40.3"},"publisher-location":"Cham","reference-count":50,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031171079"},{"type":"electronic","value":"9783031171086"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,10,1]],"date-time":"2022-10-01T00:00:00Z","timestamp":1664582400000},"content-version":"vor","delay-in-days":273,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The verification community develops two kinds of verification tools: automatic verifiers and interactive verifiers. There are many such verifiers available, and there is steady progress in research. However, cooperation between the two kinds of verifiers was not yet addressed in a modular way. Yet, it is imperative for the community to leverage all possibilities, because our society heavily depends on software systems that work correctly. This paper contributes tools and a modular design to address the open problem of insufficient support for cooperation between verification tools. We identify invariants as information that needs to be exchanged in cooperation, and we support translation between two \u2018containers\u2019 for invariants: program annotations and correctness witnesses. Using our new building blocks, invariants computed by automatic verifiers can be given to interactive verifiers as annotations in the program, and annotations from the user or interactive verifier can be given to automatic verifiers, in order to help the approaches mutually to solve the verification problem. The modular framework, and the design choice to work with readily-available components in off-the-shelf manner, opens up many opportunities to combine new tools from existing components. Our experiments on a large set of programs show that our constructions work, that is, we constructed tool combinations that can solve verification tasks that the verifiers could not solve before.<\/jats:p>","DOI":"10.1007\/978-3-031-17108-6_7","type":"book-chapter","created":{"date-parts":[[2022,9,21]],"date-time":"2022-09-21T13:04:15Z","timestamp":1663765455000},"page":"111-128","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Cooperation Between Automatic and Interactive Software Verifiers"],"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-9169-9130","authenticated-orcid":false,"given":"Martin","family":"Spiessl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5704-0404","authenticated-orcid":false,"given":"Sven","family":"Umbricht","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,10,1]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"Afzal, M., Asia, A., Chauhan, A., Chimdyalwar, B., Darke, P., Datar, A., Kumar, S., Venkatesh, R.: VeriAbs: Verification by abstraction and test generation. In: Proc. ASE. pp. 1138\u20131141 (2019). https:\/\/doi.org\/10.1109\/ASE.2019.00121","DOI":"10.1109\/ASE.2019.00121"},{"issue":"1","key":"7_CR2","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/s10270-004-0058-x","volume":"4","author":"W Ahrendt","year":"2005","unstructured":"Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., H\u00e4hnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The key tool. Software and Systems Modeling 4(1), 32\u201354 (2005). https:\/\/doi.org\/10.1007\/s10270-004-0058-x","journal-title":"Software and Systems Modeling"},{"key":"7_CR3","doi-asserted-by":"publisher","unstructured":"Alglave, J., Donaldson, A.F., Kr\u00f6ning, D., Tautschnig, M.: Making software verification tools really work. In: Proc. ATVA. pp. 28\u201342. LNCS 6996, Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-24372-1_3","DOI":"10.1007\/978-3-642-24372-1_3"},{"key":"7_CR4","doi-asserted-by":"publisher","unstructured":"Ayaziov\u00e1, P., Chalupa, M., Strej\u010dek, J.: Symbiotic-Witch: A Klee-based violation witness checker (competition contribution). In: Proc. TACAS (2). pp. 468\u2013473. LNCS 13244, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_33","DOI":"10.1007\/978-3-030-99527-0_33"},{"issue":"7","key":"7_CR5","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/1965724.1965743","volume":"54","author":"T Ball","year":"2011","unstructured":"Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with Slam. Commun. ACM 54(7), 68\u201376 (2011). https:\/\/doi.org\/10.1145\/1965724.1965743","journal-title":"Commun. ACM"},{"key":"7_CR6","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.17 (2021), available at https:\/\/frama-c.com\/download\/acsl-1.17.pdf"},{"issue":"1","key":"7_CR7","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1109\/MIS.2014.3","volume":"29","author":"B Beckert","year":"2014","unstructured":"Beckert, B., H\u00e4hnle, R.: Reasoning and verification: State of the art and current trends. IEEE Intelligent Systems 29(1), 20\u201329 (2014). https:\/\/doi.org\/10.1109\/MIS.2014.3","journal-title":"IEEE Intelligent Systems"},{"key":"7_CR8","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Progress on software verification: SV-COMP 2022. In: Proc. TACAS (2). pp. 375\u2013402. LNCS 13244, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_20","DOI":"10.1007\/978-3-030-99527-0_20"},{"key":"7_CR9","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5831003","author":"D Beyer","year":"2022","unstructured":"Beyer, D.: SV-Benchmarks: Benchmark set for software verification and testing (SV-COMP 2022 and Test-Comp 2022). Zenodo (2022). https:\/\/doi.org\/10.5281\/zenodo.5831003","journal-title":"Zenodo"},{"key":"7_CR10","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5838498","author":"D Beyer","year":"2022","unstructured":"Beyer, D.: Verification witnesses from verification tools (SV-COMP 2022). Zenodo (2022). https:\/\/doi.org\/10.5281\/zenodo.5838498","journal-title":"Zenodo"},{"key":"7_CR11","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":"7_CR12","doi-asserted-by":"publisher","DOI":"10.1145\/3477579","author":"D Beyer","year":"2022","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Lemberger, T., Tautschnig, M.: Verification witnesses. ACM Trans. Softw. Eng. Methodol. (2022). https:\/\/doi.org\/10.1145\/3477579","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"7_CR13","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":"7_CR14","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. pp. 3\u201323. LNCS 10889, Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-92994-1_1","DOI":"10.1007\/978-3-319-92994-1_1"},{"key":"7_CR15","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":"7_CR16","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":"7_CR17","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":"7_CR18","doi-asserted-by":"publisher","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Proc. CAV. pp. 184\u2013190. LNCS 6806, Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"7_CR19","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lemberger, T.: Conditional testing: Off-the-shelf combination of test-case generators. In: Proc. ATVA. pp. 189\u2013208. LNCS 11781, Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_11","DOI":"10.1007\/978-3-030-31784-3_11"},{"issue":"1","key":"7_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-017-0469-y","volume":"21","author":"D Beyer","year":"2017","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: Requirements and solutions. Int. J. Softw. Tools Technol. Transfer 21(1), 1\u201329 (2017). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"7_CR21","doi-asserted-by":"publisher","unstructured":"Beyer, D., Spiessl, M.: MetaVal: Witness validation via verification. In: Proc. CAV. pp. 165\u2013177. LNCS 12225, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_10","DOI":"10.1007\/978-3-030-53291-8_10"},{"key":"7_CR22","doi-asserted-by":"publisher","unstructured":"Beyer, D., Spiessl, M.: The static analyzer Frama-C in SV-COMP (competition contribution). In: Proc. TACAS (2). pp. 429\u2013434. LNCS 13244, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_26","DOI":"10.1007\/978-3-030-99527-0_26"},{"key":"7_CR23","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6541544","author":"D Beyer","year":"2022","unstructured":"Beyer, D., Spiessl, M., Umbricht, S.: Reproduction package for SEFM 2022 article \u2018Cooperation between automatic and interactive software verifiers\u2019. Zenodo (2022). https:\/\/doi.org\/10.5281\/zenodo.6541544","journal-title":"Zenodo"},{"key":"7_CR24","doi-asserted-by":"publisher","unstructured":"Beyer, D., Wehrheim, H.: Verification artifacts in cooperative verification: Survey and unifying component framework. In: Proc. ISoLA (1). pp. 143\u2013167. LNCS 12476, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_8","DOI":"10.1007\/978-3-030-61362-4_8"},{"key":"7_CR25","doi-asserted-by":"publisher","unstructured":"Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M., O\u2019Hearn, P.W., Papakonstantinou, I., Purbrick, J., Rodriguez, D.: Moving fast with software verification. In: Proc. NFM. pp. 3\u201311. LNCS 9058, Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_1","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"7_CR26","doi-asserted-by":"publisher","unstructured":"Chalupa, M., Strej\u010dek, J., Vitovsk\u00e1, M.: Joint forces for memory safety checking. In: Proc. SPIN. pp. 115\u2013132. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-94111-0_7","DOI":"10.1007\/978-3-319-94111-0_7"},{"key":"7_CR27","doi-asserted-by":"publisher","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Collaborative verification and testing with explicit assumptions. In: Proc. FM. pp. 132\u2013146. LNCS 7436, Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_13","DOI":"10.1007\/978-3-642-32759-9_13"},{"key":"7_CR28","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Kr\u00f6ning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Proc. TACAS. pp. 168\u2013176. LNCS 2988, Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"7_CR29","doi-asserted-by":"publisher","unstructured":"Cook, B.: Formal reasoning about the security of Amazon web services. In: Proc. CAV (2). pp. 38\u201347. LNCS 10981, Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_3","DOI":"10.1007\/978-3-319-96145-3_3"},{"key":"7_CR30","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":"7_CR31","doi-asserted-by":"publisher","unstructured":"Czech, M., Jakobs, M., Wehrheim, H.: Just test what you cannot verify! In: Proc. FASE. pp. 100\u2013114. LNCS 9033, Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46675-9_7","DOI":"10.1007\/978-3-662-46675-9_7"},{"key":"7_CR32","doi-asserted-by":"publisher","unstructured":"Ernst, G.: A complete approach to loop verification with invariants and summaries. Tech. Rep. arXiv:2010.05812v2, arXiv (January 2020). https:\/\/doi.org\/10.48550\/arXiv.2010.05812","DOI":"10.48550\/arXiv.2010.05812"},{"issue":"6","key":"7_CR33","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1007\/s10009-014-0308-3","volume":"17","author":"G Ernst","year":"2015","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV: Overview and VerifyThis competition. Int. J. Softw. Tools Technol. Transf. 17(6), 677\u2013694 (2015). https:\/\/doi.org\/10.1007\/s10009-014-0308-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"7_CR34","doi-asserted-by":"publisher","unstructured":"Ernst, G., Huisman, M., Mostowski, W., Ulbrich, M.: VerifyThis: Verification competition with a human factor. In: Proc. TACAS. pp. 176\u2013195. LNCS 11429, Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_12","DOI":"10.1007\/978-3-030-17502-3_12"},{"key":"7_CR35","doi-asserted-by":"publisher","unstructured":"Garavel, H., ter Beek, M.H., van de Pol, J.: The 2020 expert survey on formal methods. In: Proc. FMICS. pp. 3\u201369. LNCS 12327, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-58298-2_1","DOI":"10.1007\/978-3-030-58298-2_1"},{"key":"7_CR36","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":"7_CR37","doi-asserted-by":"publisher","unstructured":"Gerrard, M.J., Dwyer, M.B.: ALPACA: A large portfolio-based alternating conditional analysis. In: Atlee, J.M., Bultan, T., Whittle, J. (eds.) Proceedings of the 41st International Conference on Software Engineering: Companion Proceedings, ICSE 2019, Montreal, QC, Canada, May 25\u201331, 2019. pp. 35\u201338. IEEE \/ ACM (2019). https:\/\/doi.org\/10.1109\/ICSE-Companion.2019.00032","DOI":"10.1109\/ICSE-Companion.2019.00032"},{"issue":"1","key":"7_CR38","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s00454-009-9148-4","volume":"44","author":"TC Hales","year":"2010","unstructured":"Hales, T.C., Harrison, J., McLaughlin, S., Nipkow, T., Obua, S., Zumkeller, R.: A revision of the proof of the Kepler conjecture. Discret. Comput. Geom. 44(1), 1\u201334 (2010). https:\/\/doi.org\/10.1007\/s00454-009-9148-4","journal-title":"Discret. Comput. Geom."},{"key":"7_CR39","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Proc. CAV. pp. 36\u201352. LNCS 8044, Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_2","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"7_CR40","unstructured":"Heule, M.J.H.: The DRAT format and drat-trim checker. CoRR 1610(06229) (October 2016)"},{"key":"7_CR41","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H.: Schur number five. In: Proc. AAAI. pp. 6598\u20136606. AAAI Press (2018)","DOI":"10.1609\/aaai.v32i1.12209"},{"issue":"5","key":"7_CR42","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/s10009-014-0337-y","volume":"16","author":"F Howar","year":"2014","unstructured":"Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D., P\u0103s\u0103reanu, C.S.: Rigorous examination of reactive systems. The RERS challenges 2012 and 2013. Int. J. Softw. Tools Technol. Transfer 16(5), 457\u2013464 (2014). https:\/\/doi.org\/10.1007\/s10009-014-0337-y","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"7_CR43","doi-asserted-by":"publisher","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In: Proc. NFM. pp. 41\u201355. LNCS 6617, Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"7_CR44","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":"7_CR45","doi-asserted-by":"publisher","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","DOI":"10.1145\/3014427"},{"key":"7_CR46","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Proc. LPAR. pp. 348\u2013370. LNCS 6355, Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"7_CR47","doi-asserted-by":"publisher","unstructured":"Necula, G.C.: Proof-carrying code. In: Proc. POPL. pp. 106\u2013119. ACM (1997). https:\/\/doi.org\/10.1145\/263699.263712","DOI":"10.1145\/263699.263712"},{"key":"7_CR48","doi-asserted-by":"publisher","unstructured":"Richter, C., H\u00fcllermeier, E., Jakobs, M.-C., Wehrheim, H.: Algorithm selection for software validation based on graph kernels. Autom. Softw. Eng. 27(1), 153\u2013186 (2020). https:\/\/doi.org\/10.1007\/s10515-020-00270-x","DOI":"10.1007\/s10515-020-00270-x"},{"key":"7_CR49","doi-asserted-by":"publisher","unstructured":"Vojdani, V., Apinis, K., R\u00f5tov, V., Seidl, H., Vene, V., Vogler, R.: Static race detection for device drivers: The Goblint approach. In: Proc. ASE. pp. 391\u2013402. ACM (2016). https:\/\/doi.org\/10.1145\/2970276.2970337","DOI":"10.1145\/2970276.2970337"},{"key":"7_CR50","doi-asserted-by":"publisher","unstructured":"\u0160vejda, J., Berger, P., Katoen, J.P.: Interpretation-based violation witness validation for C: NitWit. In: Proc. TACAS. pp. 40\u201357. LNCS 12078, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_3","DOI":"10.1007\/978-3-030-45190-5_3"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-17108-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,19]],"date-time":"2024-03-19T17:05:34Z","timestamp":1710867934000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-17108-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031171079","9783031171086"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-17108-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"1 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Berlin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 September 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 September 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sefm-conference.github.io\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"39","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"49% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}