{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T13:15:02Z","timestamp":1760015702274,"version":"3.40.3"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031131844"},{"type":"electronic","value":"9783031131851"}],"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,7]],"date-time":"2022-08-07T00:00:00Z","timestamp":1659830400000},"content-version":"vor","delay-in-days":218,"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>UCLID5 is a tool for the multi-modal formal modeling, verification, and synthesis of systems. It enables one to tackle verification problems for heterogeneous systems such as combinations of hardware and software, or those that have multiple, varied specifications, or systems that require hybrid modes of modeling. A novel aspect of UCLID5 is an emphasis on the use of syntax-guided and inductive synthesis to automate steps in modeling and verification. This tool paper presents new developments in the UCLID5 tool including new language features, integration with new techniques for syntax-guided synthesis and satisfiability solving, support for hyperproperties and combinations of axiomatic and operational modeling, demonstrations on new problem classes, and a robust implementation.<\/jats:p>","DOI":"10.1007\/978-3-031-13185-1_27","type":"book-chapter","created":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T19:29:09Z","timestamp":1659814149000},"page":"538-551","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["UCLID5: Multi-modal Formal Modeling, Verification, and\u00a0Synthesis"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9032-7661","authenticated-orcid":false,"given":"Elizabeth","family":"Polgreen","sequence":"first","affiliation":[]},{"given":"Kevin","family":"Cheang","sequence":"additional","affiliation":[]},{"given":"Pranav","family":"Gaddamadugu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7704-304X","authenticated-orcid":false,"given":"Adwait","family":"Godbole","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0942-7070","authenticated-orcid":false,"given":"Kevin","family":"Laeufer","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6885-5572","authenticated-orcid":false,"given":"Shaokai","family":"Lin","sequence":"additional","affiliation":[]},{"given":"Yatin A.","family":"Manerkar","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0725-9213","authenticated-orcid":false,"given":"Federico","family":"Mora","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6190-8707","authenticated-orcid":false,"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,7]]},"reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Abate, A., et al.: Automated formal synthesis of provably safe digital controllers for continuous plants. Acta Informatica 57(1-2), 223\u2013244 (2020)","DOI":"10.1007\/s00236-019-00359-1"},{"key":"27_CR2","doi-asserted-by":"crossref","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data-mining for weak memory. ACM Trans. Programm. Lang. Syst. (TOPLAS) 36, July 2014","DOI":"10.1145\/2594291.2594347"},{"key":"27_CR3","doi-asserted-by":"crossref","unstructured":"Barbosa, H., et al.: CVC5: a versatile and industrial-strength SMT solver. In: TACAS (1), vol. 13243, pp. 415\u2013442. Springer (2022)","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"27_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_17"},{"key":"27_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24\u201340. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_5"},{"key":"27_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-45657-0_7","volume-title":"Computer Aided Verification","author":"RE Bryant","year":"2002","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 78\u201392. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_7"},{"key":"27_CR7","unstructured":"Cheang, K., Rasmussen, C., Lee, D., Kohlbrenner, D., Asanovi\u0107, K., Seshia, S.A.: Verifying RISC-V physical memory protection (2020)"},{"key":"27_CR8","doi-asserted-by":"crossref","unstructured":"Cheang, K., Rasmussen, C., Seshia, S.A., Subramanyan, P.: A formal approach to secure speculation. In: Proceedings of the Computer Security Foundations Symposium (CSF), June 2019","DOI":"10.1109\/CSF.2019.00027"},{"key":"27_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-30494-4_18","volume-title":"Formal Methods in Computer-Aided Design","author":"A Cimatti","year":"2004","unstructured":"Cimatti, A., Roveri, M., Sheridan, D.: Bounded verification of past LTL. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 245\u2013259. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30494-4_18"},{"key":"27_CR10","first-page":"86","volume":"2016","author":"V Costan","year":"2016","unstructured":"Costan, V., Devadas, S.: Intel SGX explained. IACR Cryptol. ePrint Arch. 2016, 86 (2016)","journal-title":"IACR Cryptol. ePrint Arch."},{"key":"27_CR11","unstructured":"Costan, V., Lebedev, I., Devadas, S.: Sanctum: minimal hardware extensions for strong software isolation. In: 25th USENIX Security Symposium (USENIX Security 16), pp. 857\u2013874. USENIX Association, Austin, TX (2016)"},{"key":"27_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/978-3-662-48899-7_34","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C David","year":"2015","unstructured":"David, C., Kroening, D., Lewis, M.: Using program synthesis for program analysis. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 483\u2013498. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_34"},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"Dill, D.L.: The Murphi verification system. In: CAV (1996)","DOI":"10.1007\/3-540-61474-5_86"},{"key":"27_CR14","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-319-77935-5_8","volume-title":"NASA Formal Methods","author":"B Dutertre","year":"2018","unstructured":"Dutertre, B., Jovanovi\u0107, D., Navas, J.A.: Verification of fault-tolerant protocols with Sally. In: Dutle, A., Mu\u00f1oz, C., Narkawicz, A. (eds.) NASA Formal Methods, pp. 113\u2013120. Springer, Cham (2018)"},{"key":"27_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-319-89960-2_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Fedyukovich","year":"2018","unstructured":"Fedyukovich, G., Bod\u00edk, R.: Accelerating syntax-guided invariant synthesis. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 251\u2013269. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_14"},{"key":"27_CR16","doi-asserted-by":"crossref","unstructured":"Hua, J., Zhang, M., Wang, K., Khurshid, S.: Towards practical program repair with on-demand candidate generation. In: ICSE, pp. 12\u201323. ACM (2018)","DOI":"10.1145\/3180155.3180245"},{"key":"27_CR17","unstructured":"Intel: Intel trust domain extensions (2020). https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/articles\/technical\/intel-trust-domain-extensions.html"},{"key":"27_CR18","doi-asserted-by":"crossref","unstructured":"Izraelevitz, A., et al.: Reusability is FIRRTL ground: Hardware construction languages, compiler frameworks, and transformations. In: 2017 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD), pp. 209\u2013216, November 2017","DOI":"10.1109\/ICCAD.2017.8203780"},{"key":"27_CR19","doi-asserted-by":"crossref","unstructured":"Le, X.D., Chu, D., Lo, D., Goues, C.L., Visser, W.: S3: syntax- and semantic-guided repair synthesis via programming by examples. In: ESEC\/SIGSOFT FSE, pp. 593\u2013604. ACM (2017)","DOI":"10.1145\/3106237.3106309"},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"Lee, D., Kohlbrenner, D., Shinde, S., Asanovic, K., Song, D.: Keystone: an open framework for architecting trusted execution environments. In: EuroSys, pp. 38:1\u201338:16. ACM (2020)","DOI":"10.1145\/3342195.3387532"},{"key":"27_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"27_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-030-02928-9_4","volume-title":"Engineering Trustworthy Software Systems","author":"KRM Leino","year":"2018","unstructured":"Leino, K.R.M.: Modeling concurrency in Dafny. In: Bowen, J.P., Liu, Z., Zhang, Z. (eds.) SETSS 2017. LNCS, vol. 11174, pp. 115\u2013142. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02928-9_4"},{"key":"27_CR23","doi-asserted-by":"crossref","unstructured":"Lohstroh, M., Menard, C., Bateni, S., Lee, E.A.: Toward a lingua franca for deterministic concurrent systems. ACM Trans. Embed. Comput. Syst. 20(4), 36:1\u201336:27 (2021)","DOI":"10.1145\/3448128"},{"key":"27_CR24","doi-asserted-by":"crossref","unstructured":"Lustig, D., Sethi, G., Martonosi, M., Bhattacharjee, A.: Coatcheck: verifying memory ordering at the hardware-os interface. In: ASPLOS, pp. 233\u2013247. ACM (2016)","DOI":"10.1145\/2954679.2872399"},{"key":"27_CR25","doi-asserted-by":"crossref","unstructured":"Magyar, A., Biancolin, D., Koenig, J., Seshia, S.A., Bachrach, J., Asanovic, K.: Golden Gate: Bridging the resource-efficiency gap between ASICs and FPGA prototypes. In: Proceedings of the International Conference on Computer-Aided Design (ICCAD), pp. 1\u20138, November 2019","DOI":"10.1109\/ICCAD45719.2019.8942087"},{"key":"27_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/978-3-030-81688-9_22","volume-title":"Computer Aided Verification","author":"M Mann","year":"2021","unstructured":"Mann, M., et al.: Pono: a flexible and extensible SMT-based model checker. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 461\u2013474. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_22"},{"key":"27_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-030-53291-8_12","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2020","unstructured":"McMillan, K.L., Padon, O.: Ivy: a multi-modal verification tool for distributed algorithms. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 190\u2013202. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_12"},{"key":"27_CR28","unstructured":"Mora, F., Cheang, K., Polgreen, E., Seshia, S.A.: Synthesis in UCLID5. CoRR abs\/2007.06760 (2020)"},{"key":"27_CR29","doi-asserted-by":"crossref","unstructured":"Nelson, L., Bornholt, J., Gu, R., Baumann, A., Torlak, E., Wang, X.: Scaling symbolic evaluation for automated verification of systems code with serval. In: SOSP, pp. 225\u2013242. ACM (2019)","DOI":"10.1145\/3341301.3359641"},{"key":"27_CR30","unstructured":"Padhi, S., Polgreen, E., Raghothaman, M., Reynolds, A., Udupa, A.: The SyGuS Language Standard Version 2.1 (2014). https:\/\/sygus.org\/assets\/pdf\/SyGuS-IF.pdf"},{"key":"27_CR31","doi-asserted-by":"publisher","unstructured":"Polgreen, E., et al.: UCLID5 artifact. https:\/\/doi.org\/10.5281\/zenodo.6557711. https:\/\/doi.org\/10.5281\/zenodo.6557711","DOI":"10.5281\/zenodo.6557711"},{"key":"27_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-030-94583-1_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E Polgreen","year":"2022","unstructured":"Polgreen, E., Reynolds, A., Seshia, S.A.: Satisfiability and\u00a0synthesis modulo oracles. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 263\u2013284. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_13"},{"key":"27_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-030-53288-8_11","volume-title":"Computer Aided Verification","author":"S Sahai","year":"2020","unstructured":"Sahai, S., Subramanyan, P., Sinha, R.: Verification of quantitative hyperproperties using trace enumeration relations. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 201\u2013224. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_11"},{"issue":"11","key":"27_CR34","doi-asserted-by":"publisher","first-page":"2036","DOI":"10.1109\/JPROC.2015.2471838","volume":"103","author":"SA Seshia","year":"2015","unstructured":"Seshia, S.A.: Combining induction, deduction, and structure for verification and synthesis. Proc. IEEE 103(11), 2036\u20132051 (2015)","journal-title":"Proc. IEEE"},{"key":"27_CR35","doi-asserted-by":"crossref","unstructured":"Seshia, S.A., Subramanyan, P.: UCLID5: integrating modeling, verification, synthesis and learning. In: MEMOCODE, pp. 1\u201310. IEEE (2018)","DOI":"10.1109\/MEMCOD.2018.8556946"},{"key":"27_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-10672-9_3","volume-title":"Programming Languages and Systems","author":"A Solar-Lezama","year":"2009","unstructured":"Solar-Lezama, A.: The sketching approach to program synthesis. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 4\u201313. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-10672-9_3"},{"key":"27_CR37","doi-asserted-by":"crossref","unstructured":"Subramanyan, P., Sinha, R., Lebedev, I.A., Devadas, S., Seshia, S.A.: A formal foundation for secure remote execution of enclaves. In: CCS, pp. 2435\u20132450. ACM (2017)","DOI":"10.1145\/3133956.3134098"},{"key":"27_CR38","doi-asserted-by":"crossref","unstructured":"Torlak, E., Bod\u00edk, R.: Growing solver-aided languages with rosette. In: Onward!, pp. 135\u2013152. ACM (2013)","DOI":"10.1145\/2509578.2509586"},{"key":"27_CR39","doi-asserted-by":"crossref","unstructured":"Zhang, H., Trippel, C., Manerkar, Y.A., Gupta, A., Martonosi, M., Malik, S.: ILA-MCM: integrating memory consistency models with instruction-level abstractions for heterogeneous system-on-chip verification. In: FMCAD, pp. 1\u201310 (2018)","DOI":"10.23919\/FMCAD.2018.8603015"},{"key":"27_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-030-39322-9_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H Zhang","year":"2020","unstructured":"Zhang, H., Yang, W., Fedyukovich, G., Gupta, A., Malik, S.: Synthesizing environment invariants for modular hardware verification. In: Beyer, D., Zufferey, D. (eds.) VMCAI 2020. LNCS, vol. 11990, pp. 202\u2013225. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-39322-9_10"}],"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-13185-1_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,3]],"date-time":"2022-11-03T17:14:50Z","timestamp":1667495690000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13185-1_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131844","9783031131851"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13185-1_27","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":"7 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)"}}]}}