{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T10:28:45Z","timestamp":1758709725147,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031377082"},{"type":"electronic","value":"9783031377099"}],"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,17]],"date-time":"2023-07-17T00:00:00Z","timestamp":1689552000000},"content-version":"vor","delay-in-days":197,"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 show that interactive protocols between a prover and a verifier, a well-known tool of complexity theory, can be used in practice to certify the correctness of automated reasoning tools.<\/jats:p><jats:p>Theoretically, interactive protocols exist for all <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf {PSPACE}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>PSPACE<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> problems. The verifier of a protocol checks the prover\u2019s answer to a problem instance in probabilistic polynomial time, with polynomially many bits of communication, and with exponentially small probability of error. (The prover may need exponential time.) Existing interactive protocols are not used in practice because their provers use naive algorithms, inefficient even for small instances, that are incompatible with practical implementations of automated reasoning.<\/jats:p><jats:p>We bridge the gap between theory and practice by means of an interactive protocol whose prover uses BDDs. We consider the problem of counting the number of assignments to a QBF instance (<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\#\\text {CP}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mo>#<\/mml:mo>\n                    <mml:mtext>CP<\/mml:mtext>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>), which has a natural BDD-based algorithm. We give an interactive protocol for <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\#\\text {CP}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mo>#<\/mml:mo>\n                    <mml:mtext>CP<\/mml:mtext>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> whose prover is implemented on top of an extended BDD library. The prover has only a linear overhead in computation time over the natural algorithm.<\/jats:p><jats:p>We have implemented our protocol in <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf {blic}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>blic<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, a certifying tool for <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\#\\text {CP}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mo>#<\/mml:mo>\n                    <mml:mtext>CP<\/mml:mtext>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>. Experiments on standard QBF benchmarks show that  is competitive with state-of-the-art QBF-solvers. The run time of the verifier is negligible. While loss of absolute certainty can be concerning, the error probability in our experiments is at most <jats:inline-formula><jats:alternatives><jats:tex-math>$$10^{-10}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msup>\n                    <mml:mn>10<\/mml:mn>\n                    <mml:mrow>\n                      <mml:mo>-<\/mml:mo>\n                      <mml:mn>10<\/mml:mn>\n                    <\/mml:mrow>\n                  <\/mml:msup>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> and reduces to <jats:inline-formula><jats:alternatives><jats:tex-math>$$10^{-10k}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msup>\n                    <mml:mn>10<\/mml:mn>\n                    <mml:mrow>\n                      <mml:mo>-<\/mml:mo>\n                      <mml:mn>10<\/mml:mn>\n                      <mml:mi>k<\/mml:mi>\n                    <\/mml:mrow>\n                  <\/mml:msup>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> by repeating the verification <jats:italic>k<\/jats:italic> times.<\/jats:p>","DOI":"10.1007\/978-3-031-37709-9_21","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"437-458","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Making $$\\textsf {IP}=\\textsf {PSPACE}$$ Practical: Efficient Interactive Protocols for\u00a0BDD Algorithms"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-3609-1738","authenticated-orcid":false,"given":"Eszter","family":"Couillard","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1786-9592","authenticated-orcid":false,"given":"Philipp","family":"Czerner","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9862-4919","authenticated-orcid":false,"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2136-0542","authenticated-orcid":false,"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,17]]},"reference":[{"key":"21_CR1","unstructured":"Arora, S., Barak, B.: Computational Complexity: A Modern Approach. Cambridge University Press, Cambridge (2006). https:\/\/theory.cs.princeton.edu\/complexity\/book.pdf"},{"key":"21_CR2","doi-asserted-by":"publisher","unstructured":"Babai, L.: Trading group theory for randomness. In: Sedgewick, R. (ed.) Proceedings of the 17th Annual ACM Symposium on Theory of Computing, 6\u20138 May 1985, Providence, Rhode Island, USA, pp. 421\u2013429. ACM (1985). https:\/\/doi.org\/10.1145\/22145.22192","DOI":"10.1145\/22145.22192"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-319-09284-3_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"V Balabanov","year":"2014","unstructured":"Balabanov, V., Widl, M., Jiang, J.-H.R.: QBF resolution systems and their proof complexities. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 154\u2013169. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_12"},{"key":"21_CR4","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: Flexible proof production in an industrial-strength SMT solver. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) IJCAR 2022. LNCS, vol. 13385, pp. 15\u201335. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_3","DOI":"10.1007\/978-3-031-10769-6_3"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/0-387-34799-2_4","volume-title":"Advances in Cryptology \u2014 CRYPTO\u2019 88","author":"M Ben-Or","year":"1990","unstructured":"Ben-Or, M., Goldreich, O., Goldwasser, S., H\u00e5stad, J., Kilian, J., Micali, S., Rogaway, P.: Everything provable is provable in zero-knowledge. In: Goldwasser, S. (ed.) CRYPTO 1988. LNCS, vol. 403, pp. 37\u201356. Springer, New York (1990). https:\/\/doi.org\/10.1007\/0-387-34799-2_4"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-030-99524-9_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"RE Bryant","year":"2022","unstructured":"Bryant, R.E., Biere, A., Heule, M.J.H.: Clausal proofs for pseudo-boolean reasoning. In: TACAS 2022. LNCS, vol. 13243, pp. 443\u2013461. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_25"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/978-3-030-79876-5_25","volume-title":"Automated Deduction \u2013 CADE 28","author":"RE Bryant","year":"2021","unstructured":"Bryant, R.E., Heule, M.J.H.: Dual proof generation for quantified boolean formulas with a BDD-based solver. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 433\u2013449. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_25"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-030-72016-2_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"RE Bryant","year":"2021","unstructured":"Bryant, R.E., Heule, M.J.H.: Generating extended resolution proofs with a BDD-based SAT solver. In: TACAS 2021. LNCS, vol. 12651, pp. 76\u201393. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_5"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Bryant, R.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C-35(8), 677\u2013691 (1986)","DOI":"10.1109\/TC.1986.1676819"},{"key":"21_CR10","unstructured":"CAQE (2023). https:\/\/github.com\/ltentrup\/caqe. Accessed 03 Feb 2023"},{"key":"21_CR11","doi-asserted-by":"publisher","unstructured":"Couillard, E., Czerner, P., Esparza, J., Majumdar, R.: Making IP=PSPACE practical: efficient interactive protocols for BDD algorithms. CoRR abs\/2305.11813 (2023). https:\/\/doi.org\/10.48550\/arXiv.2305.11813","DOI":"10.48550\/arXiv.2305.11813"},{"key":"21_CR12","unstructured":"DepQBF (2017). https:\/\/github.com\/lonsing\/depqbf. Accessed 03 Feb 2023"},{"key":"21_CR13","doi-asserted-by":"publisher","unstructured":"Goldwasser, S., Micali, S., Rackoff, C.: The knowledge complexity of interactive proof-systems (extended abstract). In: Sedgewick, R. (ed.) Proceedings of the 17th Annual ACM Symposium on Theory of Computing, 6\u20138 May 1985, Providence, Rhode Island, USA, pp. 291\u2013304. ACM (1985). https:\/\/doi.org\/10.1145\/22145.22178","DOI":"10.1145\/22145.22178"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/3-540-45657-0_45","volume-title":"Computer Aided Verification","author":"TA Henzinger","year":"2002","unstructured":"Henzinger, T.A., Necula, G.C., Jhala, R., Sutre, G., Majumdar, R., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 526\u2013538. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_45"},{"key":"21_CR15","doi-asserted-by":"publisher","unstructured":"Heule, M.: Everything\u2019s bigger in Texas: \u201cthe largest math proof ever\u201d. In: Benzm\u00fcller, C., Lisetti, C.L., Theobald, M. (eds.) GCAI 2017, 3rd Global Conference on Artificial Intelligence, Miami, FL, USA, 18\u201322 October 2017. EPiC Series in Computing, vol. 50, pp. 1\u20135. EasyChair (2017). https:\/\/doi.org\/10.29007\/gdw8","DOI":"10.29007\/gdw8"},{"key":"21_CR16","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H.: Proofs of unsatisfiability. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 635\u2013668. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA200998","DOI":"10.3233\/FAIA200998"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/11814948_8","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"T Jussila","year":"2006","unstructured":"Jussila, T., Sinz, C., Biere, A.: Extended resolution proofs for symbolic SAT solving with quantification. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 54\u201360. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814948_8"},{"key":"21_CR18","doi-asserted-by":"publisher","unstructured":"Katz, G., Barrett, C.W., Tinelli, C., Reynolds, A., Hadarean, L.: Lazy proofs for DPLL(T)-based SMT solvers. In: Piskac, R., Talupur, M. (eds.) 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, 3\u20136 October 2016, pp. 93\u2013100. IEEE (2016). https:\/\/doi.org\/10.1109\/FMCAD.2016.7886666","DOI":"10.1109\/FMCAD.2016.7886666"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/978-3-319-63046-5_23","volume-title":"Automated Deduction \u2013 CADE 26","author":"F Lonsing","year":"2017","unstructured":"Lonsing, F., Egly, U.: DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 371\u2013384. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_23"},{"issue":"4","key":"21_CR20","doi-asserted-by":"publisher","first-page":"859","DOI":"10.1145\/146585.146605","volume":"39","author":"C Lund","year":"1992","unstructured":"Lund, C., Fortnow, L., Karloff, H.J., Nisan, N.: Algebraic methods for interactive proof systems. J. ACM 39(4), 859\u2013868 (1992). https:\/\/doi.org\/10.1145\/146585.146605","journal-title":"J. ACM"},{"key":"21_CR21","doi-asserted-by":"publisher","unstructured":"Luo, N., Antonopoulos, T., Harris, W.R., Piskac, R., Tromer, E., Wang, X.: Proving UNSAT in zero knowledge. In: Yin, H., Stavrou, A., Cremers, C., Shi, E. (eds.) Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, CCS 2022, Los Angeles, CA, USA, 7\u201311 November 2022, pp. 2203\u20132217. ACM (2022). https:\/\/doi.org\/10.1145\/3548606.3559373","DOI":"10.1145\/3548606.3559373"},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-44585-4_2","volume-title":"Computer Aided Verification","author":"KS Namjoshi","year":"2001","unstructured":"Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 2\u201313. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_2"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Necula, G.: Proof-carrying code. In: Principles of Programming Languages, pp. 106\u2013119. ACM Press (1997)","DOI":"10.1145\/263699.263712"},{"key":"21_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-642-31612-8_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A Niemetz","year":"2012","unstructured":"Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., Biere, A.: Resolution-based certificate extraction for QBF. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 430\u2013435. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_33"},{"key":"21_CR25","unstructured":"PGBDDQ (2023). https:\/\/github.com\/rebryant\/pgbdd. Accessed 03 Feb 2023"},{"key":"21_CR26","unstructured":"QRPcheck (2023). http:\/\/fmv.jku.at\/qrpcheck\/. Accessed 03 Feb 2023"},{"key":"21_CR27","doi-asserted-by":"publisher","unstructured":"Shamir, A.: IP = PSPACE. J. ACM 39(4), 869\u2013877 (1992). https:\/\/doi.org\/10.1145\/146585.146609","DOI":"10.1145\/146585.146609"},{"key":"21_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/11753728_60","volume-title":"Computer Science \u2013 Theory and Applications","author":"C Sinz","year":"2006","unstructured":"Sinz, C., Biere, A.: Extended resolution proofs for conjoining BDDs. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol. 3967, pp. 600\u2013611. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11753728_60"},{"key":"21_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-030-24258-9_27","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2019","author":"L Tentrup","year":"2019","unstructured":"Tentrup, L., Rabe, M.N.: Clausal abstraction for DQBF. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 388\u2013405. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_27"}],"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-37709-9_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:03:47Z","timestamp":1689501827000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37709-9_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377082","9783031377099"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37709-9_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 July 2023","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":"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)"}}]}}