{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T00:20:22Z","timestamp":1767918022055,"version":"3.49.0"},"publisher-location":"Cham","reference-count":49,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031131875","type":"print"},{"value":"9783031131882","type":"electronic"}],"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,8,6]],"date-time":"2022-08-06T00:00:00Z","timestamp":1659744000000},"content-version":"vor","delay-in-days":217,"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>Requirements formalization has become increasingly popular in industrial settings as an effort to disambiguate designs and optimize development time and costs for critical system components. Formal requirements elicitation also enables the employment of analysis tools to prove important properties, such as consistency and realizability. In this paper, we present the realizability analysis framework that we developed as part of the Formal Requirements Elicitation Tool (<jats:sc>FRET<\/jats:sc>). Our framework prioritizes usability, and employs state-of-the-art analysis algorithms that support infinite theories. We demonstrate the workflow for realizability checking, showcase the diagnosis process that supports visualization of conflicts between requirements and simulation of counterexamples, and discuss results from industrial-level case studies.<\/jats:p>","DOI":"10.1007\/978-3-031-13188-2_24","type":"book-chapter","created":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T08:16:57Z","timestamp":1659687417000},"page":"490-504","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Capture, Analyze, Diagnose: Realizability Checking Of Requirements in FRET"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7013-1100","authenticated-orcid":false,"given":"Andreas","family":"Katis","sequence":"first","affiliation":[]},{"given":"Anastasia","family":"Mavridou","sequence":"additional","affiliation":[]},{"given":"Dimitra","family":"Giannakopoulou","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Pressburger","sequence":"additional","affiliation":[]},{"given":"Johann","family":"Schumann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,6]]},"reference":[{"key":"24_CR1","unstructured":"Chord diagram. https:\/\/www.data-to-viz.com\/graph\/chord.html"},{"key":"24_CR2","unstructured":"D3.js: Data-driven documents. https:\/\/d3js.org\/"},{"key":"24_CR3","unstructured":"FRET: Formal requirements elicitation tool. https:\/\/tinyurl.com\/ycxe9fv4"},{"key":"24_CR4","unstructured":"Generic infusion pump research project. https:\/\/rtg.cis.upenn.edu\/gip\/"},{"key":"24_CR5","unstructured":"Material-UI. https:\/\/mui.com\/"},{"key":"24_CR6","unstructured":"React: a javascript library for building user interfaces. https:\/\/reactjs.org\/"},{"key":"24_CR7","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org"},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-642-14295-6_37","volume-title":"Computer Aided Verification","author":"R Bloem","year":"2010","unstructured":"Bloem, R., et al.: RATSY \u2013 a new requirements analysis tool with synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 425\u2013429. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_37"},{"issue":"3","key":"24_CR9","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive (1) designs. J. Comput. Syst. Sci. 78(3), 911\u2013938 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-030-76384-8_4","volume-title":"NASA Formal Methods","author":"H Bourbouh","year":"2021","unstructured":"Bourbouh, H., et al.: Integrating formal verification and assurance: an inspection rover case study. In: Dutle, A., Moscato, M.M., Titolo, L., Mu\u00f1oz, C.A., Perez, I. (eds.) NFM 2021. LNCS, vol. 12673, pp. 53\u201371. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-76384-8_4"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1007\/978-3-319-41540-6_29","volume-title":"Computer Aided Verification","author":"A Champion","year":"2016","unstructured":"Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The Kind 2 model checker. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 510\u2013517. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_29"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-319-41528-4_6","volume-title":"Computer Aided Verification","author":"C-H Cheng","year":"2016","unstructured":"Cheng, C.-H., Hamza, Y., Ruess, H.: Structural synthesis for GXW specifications. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 95\u2013117. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_6"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-662-54577-5_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C-H Cheng","year":"2017","unstructured":"Cheng, C.-H., Lee, E.A., Ruess, H.: autoCode4: structural controller synthesis. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 398\u2013404. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_23"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-28891-3_13","volume-title":"NASA Formal Methods","author":"D Cofer","year":"2012","unstructured":"Cofer, D., Gacek, A., Miller, S., Whalen, M.W., LaValley, B., Sha, L.: Compositional verification of architectural models. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 126\u2013140. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28891-3_13"},{"key":"24_CR15","doi-asserted-by":"publisher","unstructured":"Conrad, E., Titolo, L., Giannakopoulou, D., Pressburger, T., Dutle, A.: A compositional proof framework for FRETish requirements. In: Popescu, A., Zdancewic, S. (eds.) CPP 2022, pp. 68\u201381. ACM (2022). https:\/\/doi.org\/10.1145\/3497775.3503685","DOI":"10.1145\/3497775.3503685"},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"24_CR17","doi-asserted-by":"publisher","unstructured":"Dutle, A., et al.: From requirements to autonomous flight: an overview of the monitoring ICAROUS project. In: Luckuck, M., Farrell, M. (eds.) FMAS 2020. EPTCS, vol. 329, pp. 23\u201330. Open Publishing Association (2016). https:\/\/doi.org\/10.4204\/EPTCS.329.3","DOI":"10.4204\/EPTCS.329.3"},{"key":"24_CR18","unstructured":"Elliott, C.: An example set of cyber-physical V &V challenges for S5, Lockheed Martin Skunk Works. In: Safe & Secure Systems and Software Symposium (S5) 2016, AFRL (2016). http:\/\/mys5.org\/Proceedings\/2016\/Day_2\/2016-S5-Day2_0945_Elliott.pdf"},{"key":"24_CR19","doi-asserted-by":"publisher","unstructured":"Farrell, M., Luckcuck, M., Sheridan, O., Monahan, R.: FRETting about requirements: formalised requirements for an aircraft engine controller. In: Gervasi, V., Vogelsang, A. (eds.) Requirements Engineering: Foundation for Software Quality. REFSQ 2022. LNCS, vol. 13216. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-98464-9_9","DOI":"10.1007\/978-3-030-98464-9_9"},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-030-11245-5_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G Fedyukovich","year":"2019","unstructured":"Fedyukovich, G., Gurfinkel, A., Gupta, A.: Lazy but effective functional synthesis. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 92\u2013113. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-11245-5_5"},{"key":"24_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"606","DOI":"10.1007\/978-3-662-48899-7_42","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G Fedyukovich","year":"2015","unstructured":"Fedyukovich, G., Gurfinkel, A., Sharygina, N.: Automated discovery of simulation between\u00a0programs. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 606\u2013621. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_42"},{"key":"24_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-319-57288-8_30","volume-title":"NASA Formal Methods","author":"AW Fifarek","year":"2017","unstructured":"Fifarek, A.W., Wagner, L.G., Hoffman, J.A., Rodes, B.D., Aiello, M.A., Davis, J.A.: SpeAR v2.0: formalized past LTL specification and analysis of requirements. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 420\u2013426. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_30"},{"key":"24_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-96142-2_3","volume-title":"Computer Aided Verification","author":"A Gacek","year":"2018","unstructured":"Gacek, A., Backes, J., Whalen, M., Wagner, L., Ghassabani, E.: The JKind model checker. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 20\u201327. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_3"},{"key":"24_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-319-17524-9_13","volume-title":"NASA Formal Methods","author":"A Gacek","year":"2015","unstructured":"Gacek, A., Katis, A., Whalen, M.W., Backes, J., Cofer, D.: Towards realizability checking of contracts using theories. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 173\u2013187. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_13"},{"key":"24_CR25","unstructured":"Giannakopoulou, D., Katis, A., Mavridou, A., Pressburger, T.: Compositional Realizability Checking within FRET. NASA Technical Memorandum, March 2021"},{"key":"24_CR26","unstructured":"Giannakopoulou, D., Pressburger, T., Mavridou, A., Rhein, J., Schumann, J., Shi, N.: Formal requirements elicitation with FRET. In: Mehrdad Sabetzadeh, M., Vogelsang, A., et al. (eds.) REFSQ 2020. CEUR Workshop Proceedings, vol. 2584 (2020)"},{"key":"24_CR27","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2021.106590","volume":"137","author":"D Giannakopoulou","year":"2021","unstructured":"Giannakopoulou, D., Pressburger, T., Mavridou, A., Schumann, J.: Automated formalization of structured natural language requirements. Inf. Softw. Technol. 137, 106590 (2021)","journal-title":"Inf. Softw. Technol."},{"issue":"5","key":"24_CR28","doi-asserted-by":"publisher","first-page":"741","DOI":"10.1109\/TVCG.2006.147","volume":"12","author":"D Holten","year":"2006","unstructured":"Holten, D.: Hierarchical edge bundles: visualization of adjacency relations in hierarchical data. IEEE Trans. Visual. Comput. Graph. 12(5), 741\u2013748 (2006)","journal-title":"IEEE Trans. Visual. Comput. Graph."},{"key":"24_CR29","unstructured":"Jahier, E., Raymond, P., Halbwachs, N.: The Lustre V6 reference manual"},{"key":"24_CR30","unstructured":"Katis, A.: JKind fork. https:\/\/github.com\/andreaskatis\/jkind-1"},{"key":"24_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-319-89963-3_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Katis","year":"2018","unstructured":"Katis, A., et al.: Validity-guided synthesis of reactive systems from assume-guarantee contracts. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 176\u2013193. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_10"},{"key":"24_CR32","doi-asserted-by":"crossref","unstructured":"Katis, A., Mavridou, A., Giannakopoulou, D., Pressburger, T.: Realizability checking of requirements in FRET. NASA Technical Memorandum, June 2021","DOI":"10.1007\/978-3-031-13188-2_24"},{"key":"24_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/978-3-642-19583-9_8","volume-title":"Hardware and Software: Verification and Testing","author":"R K\u00f6nighofer","year":"2011","unstructured":"K\u00f6nighofer, R., Hofferek, G., Bloem, R.: Debugging unrealizable specifications with model-based diagnosis. In: Barner, S., Harris, I., Kroening, D., Raz, O. (eds.) HVC 2010. LNCS, vol. 6504, pp. 29\u201345. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19583-9_8"},{"issue":"5\u20136","key":"24_CR34","doi-asserted-by":"publisher","first-page":"563","DOI":"10.1007\/s10009-011-0221-y","volume":"15","author":"R K\u00f6nighofer","year":"2013","unstructured":"K\u00f6nighofer, R., Hofferek, G., Bloem, R.: Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies. Int. J. Softw. Tools Technol. Transfer 15(5\u20136), 563\u2013583 (2013)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"24_CR35","doi-asserted-by":"publisher","unstructured":"Larraz, D., Tinelli, C.: Realizability checking of contracts with Kind 2 (2022). https:\/\/doi.org\/10.48550\/ARXIV.2205.09082","DOI":"10.48550\/ARXIV.2205.09082"},{"key":"24_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-319-57288-8_31","volume-title":"NASA Formal Methods","author":"L L\u00facio","year":"2017","unstructured":"L\u00facio, L., Rahman, S., Cheng, C.-H., Mavin, A.: Just formal enough? Automated analysis of EARS requirements. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 427\u2013434. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_31"},{"issue":"5","key":"24_CR37","doi-asserted-by":"publisher","first-page":"1553","DOI":"10.1007\/s10270-021-00868-z","volume":"20","author":"S Maoz","year":"2021","unstructured":"Maoz, S., Ringert, J.O.: Spectra: a specification language for reactive systems. Softw. Syst. Model. 20(5), 1553\u20131586 (2021)","journal-title":"Softw. Syst. Model."},{"key":"24_CR38","doi-asserted-by":"publisher","unstructured":"Maoz, S., Ringert, J.O., Shalom, R.: Symbolic repairs for GR(1) specifications. In: Atlee, J.M., Bultan, T, Whittle, J. (eds.) ICSE 2019, pp. 1016\u20131026. IEEE\/ACM (2019). https:\/\/doi.org\/10.1109\/ICSE.2019.00106","DOI":"10.1109\/ICSE.2019.00106"},{"key":"24_CR39","doi-asserted-by":"publisher","unstructured":"Maoz, S., Sa\u2019ar, Y.: Counter play-out: executing unrealizable scenario-based specifications. In: Notkin, D., Cheng, B.H.C., Pohl, K. (eds.) ICSE 2013, pp. 242\u2013251. IEEE (2013). https:\/\/doi.org\/10.1109\/ICSE.2013.6606570","DOI":"10.1109\/ICSE.2013.6606570"},{"key":"24_CR40","doi-asserted-by":"publisher","unstructured":"Maoz, S., Shalom, R.: Unrealizable cores for reactive systems specifications. In: ICSE 2021, pp. 25\u201336. IEEE (2021). https:\/\/doi.org\/10.1109\/ICSE43902.2021.00016","DOI":"10.1109\/ICSE43902.2021.00016"},{"key":"24_CR41","doi-asserted-by":"crossref","unstructured":"Mavin, A., Wilkinson, P., Harwood, A., Novak, M.: Easy approach to requirements syntax (EARS). In: RE (2009)","DOI":"10.1109\/RE.2009.9"},{"key":"24_CR42","doi-asserted-by":"crossref","unstructured":"Mavridou, A., et al: The ten Lockheed Martin cyber-physical challenges: formalized, analyzed, and explained. In: RE (2020)","DOI":"10.1109\/RE48521.2020.00040"},{"key":"24_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1007\/978-3-030-90870-6_27","volume-title":"Formal Methods","author":"A Mavridou","year":"2021","unstructured":"Mavridou, A., Katis, A., Giannakopoulou, D., Kooi, D., Pressburger, T., Whalen, M.W.: From partial to global assume-guarantee contracts: compositional realizability analysis in FRET. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 503\u2013523. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_27"},{"key":"24_CR44","doi-asserted-by":"publisher","unstructured":"Murugesan, A., Sokolsky, O., Rayadurgam, S., Whalen, M., Heimdahl, M., Lee, I.: Linking abstract analysis to concrete design: a hierarchical approach to verify medical CPS safety. In: ICCPS 2014, pp. 139\u2013150. IEEE (2014). https:\/\/doi.org\/10.1109\/ICCPS.2014.6843718","DOI":"10.1109\/ICCPS.2014.6843718"},{"key":"24_CR45","doi-asserted-by":"publisher","unstructured":"Perez, I., Mavridou, A., Pressburger, T., Goodloe, A., Giannakopoulou, D.: Automated translation of natural language requirements to runtime monitors. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022. LNCS, vol. 13243. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_21","DOI":"10.1007\/978-3-030-99524-9_21"},{"key":"24_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11609773_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N Piterman","year":"2006","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364\u2013380. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11609773_24"},{"key":"24_CR47","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL 1989, pp. 179\u2013190. ACM (1989). https:\/\/doi.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"key":"24_CR48","doi-asserted-by":"publisher","unstructured":"Samuel, S., D\u2019Souza, D., Komondoor, R.: GenSys: a scalable fixed-point engine for maximal controller synthesis over infinite state spaces. In: ESEC\/FSE 2021, pp. 1585\u20131589. ACM (2021). https:\/\/doi.org\/10.1145\/3468264.3473126","DOI":"10.1145\/3468264.3473126"},{"issue":"2","key":"24_CR49","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1109\/32.988498","volume":"28","author":"A Zeller","year":"2002","unstructured":"Zeller, A., Hildebrandt, R.: Simplifying and isolating failure-inducing input. IEEE Trans. Softw. Eng. 28(2), 183\u2013200 (2002)","journal-title":"IEEE Trans. Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13188-2_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,13]],"date-time":"2023-02-13T19:25:22Z","timestamp":1676316322000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13188-2_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131875","9783031131882"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13188-2_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"6 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","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":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"209","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":"40","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":"11","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":"19% - 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.9","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":"9.7","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)"}}]}}