{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T06:28:52Z","timestamp":1750746532264,"version":"3.40.3"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030587673"},{"type":"electronic","value":"9783030587680"}],"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,9,8]],"date-time":"2020-09-08T00:00:00Z","timestamp":1599523200000},"content-version":"vor","delay-in-days":251,"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>\n<jats:p>There are many hard verification problems that are currently only solvable by applying several verifiers that are based on complementing technologies. Conditional model checking (CMC) is a successful solution for cooperation between verification tools. In CMC, the first verifier outputs a condition describing the state space that it successfully verified. The second verifier uses the condition to focus its verification on the unverified state space. To use arbitrary second verifiers, we recently proposed a reducer-based approach. One can use the reducer-based approach to construct a conditional verifier from a reducer and a (non-conditional) verifier: the reducer translates the condition into a residual program that describes the unverified state space and the verifier can be any off-the-shelf verifier (that does not need to understand conditions). Until now, only one reducer was available. But for a systematic investigation of the reducer concept, we need several reducers. To fill this gap, we developed <jats:sc>FRed<\/jats:sc>, a Framework for exploring different REDucers. Given an existing reducer, <jats:sc>FRed<\/jats:sc> allows us to derive various new reducers, which differ in their trade-off between size and precision of the residual program. For our experiments, we derived seven different reducers. Our evaluation on the largest and most diverse public collection of verification problems shows that we need all seven reducers to solve hard verification tasks that were not solvable before with the considered verifiers.<\/jats:p>","DOI":"10.1007\/978-3-030-58768-0_7","type":"book-chapter","created":{"date-parts":[[2020,9,11]],"date-time":"2020-09-11T12:02:48Z","timestamp":1599825768000},"page":"113-132","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["FRed: Conditional Model Checking via Reducers and Folders"],"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"}]},{"given":"Marie-Christine","family":"Jakobs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,9,8]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"Albert, E., Puebla, G., Hermenegildo, M.V.: Abstraction-carrying code. In: Proc. LPAR, LNCS, vol. 3452, pp. 380\u2013397. Springer (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-32275-7_25","DOI":"10.1007\/978-3-540-32275-7_25"},{"key":"7_CR2","doi-asserted-by":"publisher","unstructured":"Balakrishnan, G., Sankaranarayanan, S., Ivancic, F., Wei, O., Gupta, A.: SLR: Path-sensitive analysis through infeasible-path detection and syntactic language refinement. In: Proc. SAS, LNCS, vol. 5079, pp. pp. 238\u2013254. Springer (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-69166-2_16","DOI":"10.1007\/978-3-540-69166-2_16"},{"key":"7_CR3","doi-asserted-by":"publisher","unstructured":"Beckman, N., Nori, A.V., Rajamani, S.K., Simmons, R.J.: Proofs from tests. In: Proc. ISSTA, pp. 3\u201314. ACM (2008). \nhttps:\/\/doi.org\/10.1145\/1390630.1390634","DOI":"10.1145\/1390630.1390634"},{"key":"7_CR4","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Advances in automatic software verification: SV-COMP 2020. In: Proc. TACAS (2), LNCS, vol. 12079, pp. 347\u2013367. Springer (2020). \nhttps:\/\/doi.org\/10.1007\/978-3-030-45237-7_21","DOI":"10.1007\/978-3-030-45237-7_21"},{"key":"7_CR5","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). \nhttps:\/\/doi.org\/10.1145\/2950290.2950351","DOI":"10.1145\/2950290.2950351"},{"key":"7_CR6","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). \nhttps:\/\/doi.org\/10.1145\/2786805.2786867","DOI":"10.1145\/2786805.2786867"},{"key":"7_CR7","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction with continuously-refined invariants. In: Proc. CAV, LNCS, vol. 9206, pp. 622\u2013640. Springer (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21690-4_42","DOI":"10.1007\/978-3-319-21690-4_42"},{"key":"7_CR8","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). \nhttps:\/\/doi.org\/10.1007\/978-3-319-10575-8_16","DOI":"10.1007\/978-3-319-10575-8_16"},{"key":"7_CR9","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). \nhttps:\/\/doi.org\/10.1145\/2393596.2393664","DOI":"10.1145\/2393596.2393664"},{"key":"7_CR10","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). \nhttps:\/\/doi.org\/10.1109\/ASE.2008.13","DOI":"10.1109\/ASE.2008.13"},{"key":"7_CR11","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). \nhttps:\/\/doi.org\/10.1007\/978-3-030-16722-6_23","DOI":"10.1007\/978-3-030-16722-6_23"},{"key":"7_CR12","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jakobs, M.C.: Replication package for article \u2018FRed: Conditional model checking via reducers and folders\u2019 in: Proc. SEFM 2020 (2020). \nhttps:\/\/doi.org\/10.5281\/zenodo.3953565","DOI":"10.5281\/zenodo.3953565"},{"key":"7_CR13","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). \nhttps:\/\/doi.org\/10.1145\/3180155.3180259","DOI":"10.1145\/3180155.3180259"},{"key":"7_CR14","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). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"7_CR15","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Proc. FMCAD, pp. 189\u2013197. FMCAD (2010)"},{"key":"7_CR16","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S.: Explicit-state software model checking based on CEGAR and interpolation. In: Proc. FASE, LNCS, vol. 7793, pp. 146\u2013162. Springer (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-37057-1_11","DOI":"10.1007\/978-3-642-37057-1_11"},{"issue":"1","key":"7_CR17","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). \nhttps:\/\/doi.org\/10.1007\/s10009-017-0469-y","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"7_CR18","doi-asserted-by":"publisher","unstructured":"Chebaro, O., Kosmatov, N., Giorgetti, A., Julliand, J.: Program slicing enhances a verification technique combining static and dynamic analysis. In: Proc. SAC, pp. 1284\u20131291. ACM (2012). \nhttps:\/\/doi.org\/10.1145\/2245276.2231980","DOI":"10.1145\/2245276.2231980"},{"key":"7_CR19","doi-asserted-by":"publisher","unstructured":"Christakis, M., M\u00fcller, P., W\u00fcstholz, V.: Collaborative verification and testing with explicit assumptions. In: Proc. FM, LNCS, vol. 7436, pp. 132\u2013146. Springer (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-32759-9_13","DOI":"10.1007\/978-3-642-32759-9_13"},{"key":"7_CR20","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). \nhttps:\/\/doi.org\/10.1145\/2884781.2884843","DOI":"10.1145\/2884781.2884843"},{"key":"7_CR21","doi-asserted-by":"publisher","unstructured":"Christakis, M., W\u00fcstholz, V.: Bounded abstract interpretation. In: Proc. SAS, LNCS, vol. 9837, pp. 105\u2013125. Springer (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-662-53413-7_6","DOI":"10.1007\/978-3-662-53413-7_6"},{"key":"7_CR22","doi-asserted-by":"publisher","unstructured":"Cocke, J.: Global common subexpression elimination. In: Proc. Symposium on Compiler Optimization, pp. 20\u201324. ACM (1970). \nhttps:\/\/doi.org\/10.1145\/800028.808480","DOI":"10.1145\/800028.808480"},{"key":"7_CR23","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Systematic design of program-analysis frameworks. In: Proc. POPL, pp. 269\u2013282. ACM (1979). \nhttps:\/\/doi.org\/10.1145\/567752.567778","DOI":"10.1145\/567752.567778"},{"key":"7_CR24","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: Combination of abstractions in the ASTR\u00c9E static analyzer. In: Proc. ASIAN\u201906, LNCS, vol. 4435, pp. 272\u2013300. Springer (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-77505-8_23","DOI":"10.1007\/978-3-540-77505-8_23"},{"key":"7_CR25","doi-asserted-by":"publisher","unstructured":"Csallner, C., Smaragdakis, Y.: Check \u2018n\u2019 Crash: Combining static checking and testing. In: Proc. ICSE, pp. 422\u2013431. ACM (2005). \nhttps:\/\/doi.org\/10.1145\/1062455.1062533","DOI":"10.1145\/1062455.1062533"},{"key":"7_CR26","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). \nhttps:\/\/doi.org\/10.1007\/978-3-662-46675-9_7","DOI":"10.1007\/978-3-662-46675-9_7"},{"key":"7_CR27","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). \nhttps:\/\/doi.org\/10.1007\/978-3-662-49122-5_16","DOI":"10.1007\/978-3-662-49122-5_16"},{"key":"7_CR28","doi-asserted-by":"publisher","unstructured":"Dams, D., Namjoshi, K.S.: Orion: High-precision methods for static error analysis of C and C++ programs. In: Proc. FMCO, LNCS, vol. 4111, pp. 138\u2013160. Springer (2005). \nhttps:\/\/doi.org\/10.1007\/11804192_7","DOI":"10.1007\/11804192_7"},{"key":"7_CR29","doi-asserted-by":"publisher","unstructured":"Dangl, M., L\u00f6we, S., Wendler, P.: CPAchecker with support for recursive programs and floating-point arithmetic (competition contribution). In: Proc. TACAS, LNCS, vol. 9035, pp. 423\u2013425. Springer (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-662-46681-0_34","DOI":"10.1007\/978-3-662-46681-0_34"},{"key":"7_CR30","doi-asserted-by":"publisher","unstructured":"Darke, P., Prabhu, S., Chimdyalwar, B., Chauhan, A., Kumar, S., Chowdhury, A.B., Venkatesh, R., Datar, A., Medicherla, R.K.: VeriAbs: Verification by abstraction and test generation (competition contribution). In: Proc. TACAS, LNCS, vol. 10806, pp. 457\u2013462. Springer (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-89963-3_32","DOI":"10.1007\/978-3-319-89963-3_32"},{"issue":"7","key":"7_CR31","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","volume":"27","author":"V D\u2019Silva","year":"2008","unstructured":"D\u2019Silva, V., Kr\u00f6ning, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. CAD Integr. Circ. Syst. 27(7), 1165\u20131178 (2008). \nhttps:\/\/doi.org\/10.1109\/TCAD.2008.923410","journal-title":"IEEE Trans. CAD Integr. Circ. Syst."},{"key":"7_CR32","doi-asserted-by":"publisher","unstructured":"Ferles, K., W\u00fcstholz, V., Christakis, M., Dillig, I.: Failure-directed program trimming. In: Proc. ESEC\/FSE, pp. 174\u2013185. ACM (2017). \nhttps:\/\/doi.org\/10.1145\/3106237.3106249","DOI":"10.1145\/3106237.3106249"},{"key":"7_CR33","doi-asserted-by":"publisher","unstructured":"Fischer, J., Jhala, R., Majumdar, R.: Joining data flow with predicates. In: Proc. FSE, pp. 227\u2013236. ACM (2005). \nhttps:\/\/doi.org\/10.1145\/1081706.1081742","DOI":"10.1145\/1081706.1081742"},{"key":"7_CR34","doi-asserted-by":"publisher","unstructured":"Gadelha, M.Y.R., Monteiro, F.R., Cordeiro, L.C., Nicole, D.A.: Esbmc v6.0: Verifying C programs using $$k$$-induction and invariant inference (competition contribution). In: Proc. TACAS (3), LNCS, vol. 11429, pp. 209\u2013213. Springer (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-17502-3_15","DOI":"10.1007\/978-3-030-17502-3_15"},{"key":"7_CR35","doi-asserted-by":"publisher","unstructured":"Ge, X., Taneja, K., Xie, T., Tillmann, N.: DyTa: Dynamic symbolic execution guided with static verification results. In: Proc. ICSE, pp. 992\u2013994. ACM (2011). \nhttps:\/\/doi.org\/10.1145\/1985793.1985971","DOI":"10.1145\/1985793.1985971"},{"key":"7_CR36","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). \nhttps:\/\/doi.org\/10.1145\/1706299.1706307","DOI":"10.1145\/1706299.1706307"},{"key":"7_CR37","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). \nhttps:\/\/doi.org\/10.1145\/1181775.1181790","DOI":"10.1145\/1181775.1181790"},{"key":"7_CR38","doi-asserted-by":"publisher","unstructured":"Gulwani, S., Jain, S., Koskinen, E.: Control-flow refinement and progress invariants for bound analysis. In: Proc. PLDI, pp. 375\u2013385. ACM (2009). \nhttps:\/\/doi.org\/10.1145\/1542476.1542518","DOI":"10.1145\/1542476.1542518"},{"key":"7_CR39","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G.C., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Proc. CAV, LNCS, vol. 2404, pp. 526\u2013538. Springer (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45657-0_45","DOI":"10.1007\/3-540-45657-0_45"},{"key":"7_CR40","doi-asserted-by":"publisher","unstructured":"Holley, L.H., Rosen, B.K.: Qualified data-flow problems. In: Proc. POPL, pp. 68\u201382. ACM (1980). \nhttps:\/\/doi.org\/10.1145\/567446.567454","DOI":"10.1145\/567446.567454"},{"key":"7_CR41","doi-asserted-by":"publisher","unstructured":"Jakobs, M.C., Wehrheim, H.: Certification for configurable program analysis. In: Proc. SPIN, pp. 30\u201339. ACM (2014). \nhttps:\/\/doi.org\/10.1145\/2632362.2632372","DOI":"10.1145\/2632362.2632372"},{"issue":"2","key":"7_CR42","doi-asserted-by":"publisher","first-page":"7:1","DOI":"10.1145\/3014427","volume":"39","author":"MC Jakobs","year":"2017","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). \nhttps:\/\/doi.org\/10.1145\/3014427","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR43","doi-asserted-by":"publisher","unstructured":"Jalote, P., Vangala, V., Singh, T., Jain, P.: Program partitioning: A framework for combining static and dynamic analysis. In: Proc. WODA, pp. 11\u201316. ACM (2006). \nhttps:\/\/doi.org\/10.1145\/1138912.1138916","DOI":"10.1145\/1138912.1138916"},{"key":"7_CR44","doi-asserted-by":"publisher","unstructured":"Li, K., Reichenbach, C., Csallner, C., Smaragdakis, Y.: Residual investigation: predictive and precise bug detection. In: Proc. ISSTA, pp. 298\u2013308. ACM (2012). \nhttps:\/\/doi.org\/10.1145\/2338965.2336789","DOI":"10.1145\/2338965.2336789"},{"key":"7_CR45","doi-asserted-by":"publisher","unstructured":"Necula, G.C.: Proof-carrying code. In: Proc. POPL, pp. 106\u2013119. ACM (1997). \nhttps:\/\/doi.org\/10.1145\/263699.263712","DOI":"10.1145\/263699.263712"},{"key":"7_CR46","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). \nhttps:\/\/doi.org\/10.1145\/503272.503286","DOI":"10.1145\/503272.503286"},{"key":"7_CR47","doi-asserted-by":"publisher","unstructured":"Post, H., Sinz, C., Kaiser, A., Gorges, T.: Reducing false positives by combining abstract interpretation and bounded model checking. In: Proc. ASE, pp. 188\u2013197. IEEE (2008). \nhttps:\/\/doi.org\/10.1109\/ASE.2008.29","DOI":"10.1109\/ASE.2008.29"},{"key":"7_CR48","doi-asserted-by":"publisher","unstructured":"Sharma, R., Dillig, I., Dillig, T., Aiken, A.: Simplifying loop-invariant generation using splitter predicates. In: Proc. CAV, LNCS, vol. 6806, pp. 703\u2013719. Springer (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22110-1_57","DOI":"10.1007\/978-3-642-22110-1_57"},{"key":"7_CR49","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). \nhttps:\/\/doi.org\/10.1007\/978-3-319-89963-3_15","DOI":"10.1007\/978-3-319-89963-3_15"},{"key":"7_CR50","doi-asserted-by":"publisher","unstructured":"Steffen, B.: Property-oriented expansion. In: Proc. SAS, LNCS, vol. 1145, pp. 22\u201341. Springer (1996). \nhttps:\/\/doi.org\/10.1007\/3-540-61739-6_31","DOI":"10.1007\/3-540-61739-6_31"},{"key":"7_CR51","doi-asserted-by":"publisher","unstructured":"Thakur, A.V., Govindarajan, R.: Comprehensive path-sensitive data-flow analysis. In: Proc. CGO, pp. 55\u201363. ACM (2008). \nhttps:\/\/doi.org\/10.1145\/1356058.1356066","DOI":"10.1145\/1356058.1356066"},{"key":"7_CR52","doi-asserted-by":"publisher","unstructured":"Wegman, M.N., Zadeck, F.K.: Constant propagation with conditional branches. In: Proc. POPL, pp. 291\u2013299. ACM (1985). \nhttps:\/\/doi.org\/10.1145\/318593.318659","DOI":"10.1145\/318593.318659"},{"key":"7_CR53","doi-asserted-by":"publisher","unstructured":"Yin, X., Knight, J.C., Weimer, W.: Exploiting refactoring in formal verification. In: Proc. DSN, pp. 53\u201362. IEEE (2009). \nhttps:\/\/doi.org\/10.1109\/DSN.2009.5270355","DOI":"10.1109\/DSN.2009.5270355"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-58768-0_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,11]],"date-time":"2020-09-11T12:05:23Z","timestamp":1599825923000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-58768-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030587673","9783030587680"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-58768-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"8 September 2020","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":"Amsterdam","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"The Netherlands","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":"14 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 September 2020","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":"sefm2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/event.cwi.nl\/sefm2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}