{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,19]],"date-time":"2026-01-19T02:25:43Z","timestamp":1768789543981,"version":"3.49.0"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031377020","type":"print"},{"value":"9783031377037","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,18]],"date-time":"2023-07-18T00:00:00Z","timestamp":1689638400000},"content-version":"vor","delay-in-days":198,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present the verified model checker <jats:sc>CoqCryptoLine<\/jats:sc> for cryptographic programs with certified verification results. The <jats:sc>CoqCryptoLine<\/jats:sc> verification algorithm consists of two reductions. The algebraic reduction transforms into a root entailment problem; and the bit-vector reduction transforms into an <jats:sc>SMT<\/jats:sc><jats:sc>QF_BV<\/jats:sc> problem. We specify and verify both reductions formally using <jats:sc>Coq<\/jats:sc> with <jats:sc>MathComp<\/jats:sc>. The <jats:sc>CoqCryptoLine<\/jats:sc> tool is built on the <jats:sc>OCaml<\/jats:sc> programs extracted from verified reductions. <jats:sc>CoqCryptoLine<\/jats:sc> moreover employs certified techniques for solving the algebraic and logic problems. We evaluate <jats:sc>CoqCryptoLine<\/jats:sc> on cryptographic programs from industrial security libraries.<\/jats:p>","DOI":"10.1007\/978-3-031-37703-7_11","type":"book-chapter","created":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T17:02:15Z","timestamp":1689613335000},"page":"227-240","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["CoqCryptoLine: A Verified Model Checker with\u00a0Certified Results"],"prefix":"10.1007","author":[{"given":"Ming-Hsien","family":"Tsai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yu-Fu","family":"Fu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jiaxiang","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaomu","family":"Shi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bow-Yaw","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bo-Yin","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,7,18]]},"reference":[{"key":"11_CR1","unstructured":"CoqCryptoLine GitHub repository (2023). https:\/\/github.com\/fmlab-iis\/coq-cryptoline"},{"issue":"2","key":"11_CR2","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/s11334-013-0195-x","volume":"9","author":"R Affeldt","year":"2013","unstructured":"Affeldt, R.: On construction of a library of formally verified low-level arithmetic functions. Innov. Syst. Softw. Eng. 9(2), 59\u201377 (2013)","journal-title":"Innov. Syst. Softw. Eng."},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Almeida, J.B., et al.: Jasmin: High-assurance and high-speed cryptography. In: ACM SIGSAC Conference on Computer and Communications Security, pp. 1807\u20131823. ACM (2017)","DOI":"10.1145\/3133956.3134078"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Appel, A.W.: Verification of a cryptographic primitive: SHA-256. ACM Trans. Programm. Lang. Syst. 37(2), 7:1\u20137:31 (2015)","DOI":"10.1145\/2701415"},{"key":"11_CR5","doi-asserted-by":"publisher","unstructured":"Barbosa, M., et al.: Sok: Computer-aided cryptography. In: 42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021, pp. 777\u2013795. IEEE (2021). https:\/\/doi.org\/10.1109\/SP40001.2021.00008","DOI":"10.1109\/SP40001.2021.00008"},{"key":"11_CR6","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)"},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, Springer (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"key":"11_CR8","doi-asserted-by":"publisher","unstructured":"Beyer, D., Keremoglu, M.E.: Cpachecker: A tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06806, pp. 184\u2013190. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"11_CR9","unstructured":"Bond, B., et al.: Vale: Verifying high-performance cryptographic assembly code. In: USENIX Security Symposium, pp. 917\u2013934. USENIX Association (2017)"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Bos, J., et al.: CRYSTALS - Kyber: a CCA-secure module-lattice-based KEM. In: Smith, M., Piessens, F. (eds.) IEEE European Symposium on Security and Privacy, pp. 353\u2013367. IEEE (2018)","DOI":"10.1109\/EuroSP.2018.00032"},{"key":"11_CR11","doi-asserted-by":"publisher","unstructured":"Chalupa, M., Strejcek, J.: Evaluation of program slicing in software verification. In: Ahrendt, W., Tarifa, S.L.T. (eds.) Integrated Formal Methods - 15th International Conference, IFM 2019, Bergen, Norway, December 2-6, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11918, pp. 101\u2013119. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-34968-4_6","DOI":"10.1007\/978-3-030-34968-4_6"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Chen, Y.F., et al.: Verifying Curve25519 software. In: Ahn, G.J., Yung, M., Li, N. (eds.) ACM SIGSAC Conference on Computer and Communications Security, pp. 299\u2013309. ACM (2014)","DOI":"10.1145\/2660267.2660370"},{"key":"11_CR13","doi-asserted-by":"publisher","unstructured":"Cimatti, A., et al.: NuSMV 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings. Lecture Notes in Computer Science, vol.\u00a02404, pp. 359\u2013364. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29","DOI":"10.1007\/3-540-45657-0_29"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A.: Simple high-level code for cryptographic arithmetic - with proofs, without compromises. In: IEEE Symposium on Security and Privacy, pp. 1202\u20131219. IEEE (2019)","DOI":"10.1109\/SP.2019.00005"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.: A fully verified executable LTL model checker. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a08044, pp. 463\u2013478. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_31","DOI":"10.1007\/978-3-642-39799-8_31"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Fu, Y.F., Liu, J., Shi, X., Tsai, M.H., Wang, B.Y., Yang, B.Y.: Signed cryptographic program verification with typed cryptoline. In: Cavallaro, L., Kinder, J., Wang, X., Katz, J. (eds.) ACM SIGSAC Conference on Computer and Communications Security, pp. 1591\u20131606. ACM (2019)","DOI":"10.1145\/3319535.3354199"},{"issue":"2","key":"11_CR17","first-page":"95","volume":"3","author":"G Gonthier","year":"2010","unstructured":"Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. J. Formalized Reason. 3(2), 95\u2013152 (2010)","journal-title":"J. Formalized Reason."},{"key":"11_CR18","unstructured":"Google: Boringssl (2021). https:\/\/boringssl.googlesource.com\/boringssl\/"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Greuel, G.M., Pfister, G.: A Singular Introduction to Commutative Algebra. Springer-Verlag (2002)","DOI":"10.1007\/978-3-662-04963-1"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-540-73595-3_5","volume-title":"Automated Deduction \u2013 CADE-21","author":"J Harrison","year":"2007","unstructured":"Harrison, J.: Automating elementary number-theoretic proofs using Gr\u00f6bner bases. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 51\u201366. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_5"},{"key":"11_CR21","unstructured":"Holzmann, G.J.: The SPIN Model Checker - primer and reference manual. Addison-Wesley (2004)"},{"key":"11_CR22","unstructured":"Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002). http:\/\/research.microsoft.com\/users\/lamport\/tla\/book.html"},{"key":"11_CR23","doi-asserted-by":"publisher","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1-2), 134\u2013152 (1997). https:\/\/doi.org\/10.1007\/s100090050010","DOI":"10.1007\/s100090050010"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Liu, J., Shi, X., Tsai, M.H., Wang, B.Y., Yang, B.Y.: Verifying arithmetic in cryptographic C programs. In: Lawall, J., Marinov, D. (eds.) IEEE\/ACM International Conference on Automated Software Engineering, pp. 552\u2013564. IEEE (2019)","DOI":"10.1109\/ASE.2019.00058"},{"key":"11_CR25","unstructured":"Mozilla: Network security services (2021). https:\/\/developer.mozilla.org\/en-US\/docs\/Mozilla\/Projects\/NSS"},{"key":"11_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-319-03545-1_5","volume-title":"Certified Programs and Proofs","author":"MO Myreen","year":"2013","unstructured":"Myreen, M.O., Curello, G.: Proof Pearl: a verified bignum implementation in x86-64 machine code. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 66\u201381. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-03545-1_5"},{"key":"11_CR27","doi-asserted-by":"publisher","unstructured":"Neumann, R.: Using promela in a fully verified executable LTL model checker. In: Giannakopoulou, D., Kroening, D. (eds.) Verified Software: Theories, Tools and Experiments - 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers. Lecture Notes in Computer Science, vol.\u00a08471, pp. 105\u2013114. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-12154-3_7","DOI":"10.1007\/978-3-319-12154-3_7"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Boolector 2.0. J. Satisfiability, Boolean Modeling Comput. 9(1), 53\u201358 (2014)","DOI":"10.3233\/SAT190101"},{"key":"11_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"11_CR30","unstructured":"OpenSSL: OpenSSL library. https:\/\/github.com\/openssl\/openssl (2021)"},{"key":"11_CR31","unstructured":"Polyakov, A., Tsai, M.H., Wang, B.Y., Yang, B.Y.: Verifying arithmetic assembly programs in cryptographic primitives. In: Schewe, S., Zhang, L. (eds.) International Conference on Concurrency Theory, pp. 4:1\u20134:16. LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2018)"},{"key":"11_CR32","unstructured":"Pottier, L.: Connecting Gr\u00f6bner bases programs with Coq to do proofs in algebra, geometry and arithmetics. In: Rudnicki, P., Sutcliffe, G., Konev, B., Schmidt, R.A., Schulz, S. (eds.) Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, Doha, Qatar, November 22, 2008. CEUR Workshop Proceedings, vol.\u00a0418. CEUR-WS.org (2008). http:\/\/ceur-ws.org\/Vol-418\/paper5.pdf"},{"key":"11_CR33","volume-title":"International Conference on Computer Aided Verification","author":"X Shi","year":"2021","unstructured":"Shi, X., Fu, Y.F., Liu, J., Tsai, M.H., Wang, B.Y., Yang, B.Y.: CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver. In: Leino, R., Silva, A. (eds.) International Conference on Computer Aided Verification. Springer, Lecture Notes in Computer Science (2021)"},{"key":"11_CR34","doi-asserted-by":"publisher","unstructured":"Sprenger, C.: A verified model checker for the modal $$\\rm \\mu $$-calculus in Coq. In: Steffen, B. (ed.) Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS \u201998, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS\u201998, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings. Lecture Notes in Computer Science, vol.\u00a01384, pp. 167\u2013183. Springer (1998). https:\/\/doi.org\/10.1007\/BFb0054171","DOI":"10.1007\/BFb0054171"},{"key":"11_CR35","unstructured":"The Bitcoin Developers: Bitcoin source code (2021). https:\/\/github.com\/bitcoin\/bitcoin"},{"key":"11_CR36","unstructured":"Tsai, M.H., Fu, Y.F., Shi, X., Liu, J., Wang, B.Y., Yang, B.Y.: Automatic certified verification of cryptographic programs with COQCRYPTOLINE. IACR Cryptol. ePrint Arch. p. 1116 (2022)"},{"key":"11_CR37","doi-asserted-by":"crossref","unstructured":"Tsai, M.H., Wang, B.Y., Yang, B.Y.: Certified verification of algebraic properties on low-level mathematical constructs in cryptographic programs. In: Evans, D., Malkin, T., Xu, D. (eds.) ACM SIGSAC Conference on Computer and Communications Security, pp. 1973\u20131987. ACM (2017)","DOI":"10.1145\/3133956.3134076"},{"key":"11_CR38","doi-asserted-by":"publisher","unstructured":"Wimmer, S.: Munta: A verified model checker for timed automata. In: Andr\u00e9, \u00c9., Stoelinga, M. (eds.) Formal Modeling and Analysis of Timed Systems - 17th International Conference, FORMATS 2019, Amsterdam, The Netherlands, August 27-29, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11750, pp. 236\u2013243. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-29662-9_14","DOI":"10.1007\/978-3-030-29662-9_14"},{"key":"11_CR39","doi-asserted-by":"publisher","unstructured":"Wimmer, S., Lammich, P.: Verified model checking of timed automata. In: Beyer, D., Huisman, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10805, pp. 61\u201378. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_4","DOI":"10.1007\/978-3-319-89960-2_4"},{"key":"11_CR40","doi-asserted-by":"crossref","unstructured":"Zinzindohou\u00e9, J.K., Bhargavan, K., Protzenko, J., Beurdouche, B.: HACL*: A verified modern cryptographic library. In: ACM SIGSAC Conference on Computer and Communications Security, pp. 1789\u20131806. ACM (2017)","DOI":"10.1145\/3133956.3134043"}],"updated-by":[{"DOI":"10.1007\/978-3-031-37703-7_22","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2023,8,27]],"date-time":"2023-08-27T00:00:00Z","timestamp":1693094400000}}],"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-37703-7_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,26]],"date-time":"2023-08-26T11:04:26Z","timestamp":1693047866000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37703-7_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377020","9783031377037"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37703-7_11","relation":{"correction":[{"id-type":"doi","id":"10.1007\/978-3-031-37703-7_22","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"18 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"27 August 2023","order":2,"name":"change_date","label":"Change Date","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"Correction","order":3,"name":"change_type","label":"Change Type","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"A correction has been published.","order":4,"name":"change_details","label":"Change Details","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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","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":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","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":"67","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":"0","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":"26% - 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":"11","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)"}}]}}