{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T05:29:56Z","timestamp":1743053396155,"version":"3.40.3"},"publisher-location":"Cham","reference-count":51,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030993351"},{"type":"electronic","value":"9783030993368"}],"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,3,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":87,"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>Quantitative separation logic () is an extension of separation logic () for the verification of probabilistic pointer programs. In , formulae evaluate to real numbers instead of truth values, e.g., the probability of memory-safe termination in a given symbolic heap. As with , one of the key problems when reasoning with  is <jats:italic>entailment<\/jats:italic>: does a formula <jats:italic>f<\/jats:italic> entail another formula <jats:italic>g<\/jats:italic>?<\/jats:p><jats:p>We give a generic reduction from entailment checking in  to entailment checking in . This allows to leverage the large body of  research for the automated verification of probabilistic pointer programs. We analyze the complexity of our approach and demonstrate its applicability. In particular, we obtain the first decidability results for the verification of such programs by applying our reduction to a quantitative extension of the well-known symbolic-heap fragment of separation logic.<\/jats:p>","DOI":"10.1007\/978-3-030-99336-8_3","type":"book-chapter","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:02:48Z","timestamp":1648497768000},"page":"57-84","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Foundations for Entailment Checking in Quantitative Separation Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8705-2564","authenticated-orcid":false,"given":"Kevin","family":"Batz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7837-2611","authenticated-orcid":false,"given":"Ira","family":"Fesefeldt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marvin","family":"Jansen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Ke\u00dfler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9151-0441","authenticated-orcid":false,"given":"Christoph","family":"Matheja","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1865-1798","authenticated-orcid":false,"given":"Thomas","family":"Noll","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,29]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Antonopoulos, T., Gorogiannis, N., Haase, C., Kanovich, M.I., Ouaknine, J.: Foundations for decision problems in separation logic with general inductive predicates. In: FoSSaCS. Lecture Notes in Computer Science, vol.\u00a08412, pp. 411\u2013425. Springer (2014)","DOI":"10.1007\/978-3-642-54830-7_27"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Baier, C., Engel, B., Kl\u00fcppelholz, S., M\u00e4rcker, S., Tews, H., V\u00f6lp, M.: A probabilistic quantitative analysis of probabilistic-write\/copy-select. In: NASA Formal Methods. LNCS, vol.\u00a07871, pp. 307\u2013321. Springer (2013)","DOI":"10.1007\/978-3-642-38088-4_21"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Bao, J., Docherty, S., Hsu, J., Silva, A.: A bunched logic for conditional independence. In: LICS. pp. 1\u201314. IEEE (2021)","DOI":"10.1109\/LICS52264.2021.9470712"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., Hsu, J., Strub, P.Y.: Coupling proofs are probabilistic product programs. In: POPL. p. 161\u2013174. ACM (2017)","DOI":"10.1145\/3009837.3009896"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Barthe, G., Hsu, J., Liao, K.: A probabilistic separation logic. Proc. ACM Program. Lang. 4(POPL), 55:1\u201355:30 (2020)","DOI":"10.1145\/3371123"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Batz, K., Chen, M., Kaminski, B.L., Katoen, J., Matheja, C., Schr\u00f6er, P.: Latticed k-induction with an application to probabilistic programs. In: CAV (2). Lecture Notes in Computer Science, vol. 12760, pp. 524\u2013549. Springer (2021)","DOI":"10.1007\/978-3-030-81688-9_25"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Batz, K., Fesefeldt, I., Jansen, M., Katoen, J.P., Ke\u00dfler, F., Matheja, C., Noll, T.: Foundations for entailment checking in quantitative separation logic (extended version). CoRR abs\/2201.11464 (2022)","DOI":"10.1007\/978-3-030-99336-8_3"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Batz, K., Kaminski, B.L., Katoen, J., Matheja, C.: Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. Proc. ACM Program. Lang. 5(POPL), 1\u201330 (2021)","DOI":"10.1145\/3434320"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Batz, K., Kaminski, B.L., Katoen, J., Matheja, C., Noll, T.: Quantitative separation logic: a logic for reasoning about probabilistic pointer programs. Proc. ACM Program. Lang. 3(POPL), 34:1\u201334:29 (2019)","DOI":"10.1145\/3290347"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W., Wies, T., Yang, H.: Shape analysis for composite data structures. In: CAV. Lecture Notes in Computer Science, vol.\u00a04590, pp. 178\u2013192. Springer (2007)","DOI":"10.1007\/978-3-540-73368-3_22"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: A decidable fragment of separation logic. In: FSTTCS. Lecture Notes in Computer Science, vol.\u00a03328, pp. 97\u2013109. Springer (2004)","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: FMCO. Lecture Notes in Computer Science, vol.\u00a04111, pp. 115\u2013137. Springer (2005)","DOI":"10.1007\/11804192_6"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: APLAS. Lecture Notes in Computer Science, vol.\u00a03780, pp. 52\u201368. Springer (2005)","DOI":"10.1007\/11575467_5"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 26:1\u201326:66 (2011)","DOI":"10.1145\/2049697.2049700"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Carbin, M., Misailovic, S., Rinard, M.C.: Verifying quantitative reliability for programs that execute on unreliable hardware. Commun. ACM 59(8), 83\u201391 (2016)","DOI":"10.1145\/2958738"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Chin, W., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77(9), 1006\u20131036 (2012)","DOI":"10.1016\/j.scico.2010.07.004"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Cook, B., Haase, C., Ouaknine, J., Parkinson, M.J., Worrell, J.: Tractable reasoning in a fragment of separation logic. In: CONCUR. Lecture Notes in Computer Science, vol.\u00a06901, pp. 235\u2013249. Springer (2011)","DOI":"10.1007\/978-3-642-23217-6_16"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Demri, S., Lozes, \u00c9., Mansutti, A.: The effects of adding reachability predicates in propositional separation logic. In: Foundations of Software Science and Computation Structures. LNCS, vol. 10803, pp. 476\u2013493. Springer (2018)","DOI":"10.1007\/978-3-319-89366-2_26"},{"key":"3_CR19","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall (1976)"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Echenim, M., Iosif, R., Peltier, N.: The Bernays-Sch\u00f6nfinkel-Ramsey class of separation logic with uninterpreted predicates. ACM Trans. Comput. Log. 21(3), 19:1\u201319:46 (2020)","DOI":"10.1145\/3380809"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Echenim, M., Iosif, R., Peltier, N.: Decidable entailments in separation logic with inductive definitions: Beyond establishment. In: CSL. LIPIcs, vol.\u00a0183, pp. 20:1\u201320:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021)","DOI":"10.1007\/978-3-030-79876-5_11"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Echenim, M., Iosif, R., Peltier, N.: Unifying decidable entailments in separation logic with inductive definitions. In: CADE. Lecture Notes in Computer Science, vol. 12699, pp. 183\u2013199. Springer (2021)","DOI":"10.1007\/978-3-030-79876-5_11"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: FOSE. pp. 167\u2013181. ACM (2014)","DOI":"10.1145\/2593882.2593900"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: PLDI. pp. 266\u2013277. ACM (2007)","DOI":"10.1145\/1250734.1250765"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Gretz, F., Katoen, J.P., McIver, A.: Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Performance Evaluation 73, 110\u2013132 (2014)","DOI":"10.1016\/j.peva.2013.11.004"},{"key":"3_CR26","unstructured":"Haslbeck, M.P.L.: Verified Quantitative Analysis of Imperative Algorithms. Ph.D. thesis, Technical University of Munich, Germany (2021)"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Iosif, R., Rogalewicz, A., Sim\u00e1cek, J.: The tree width of separation logic with recursive definitions. In: CADE. Lecture Notes in Computer Science, vol.\u00a07898, pp. 21\u201338. Springer (2013)","DOI":"10.1007\/978-3-642-38574-2_2"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Iosif, R., Rogalewicz, A., Vojnar, T.: Deciding entailments in inductive separation logic with tree automata. In: ATVA. Lecture Notes in Computer Science, vol.\u00a08837, pp. 201\u2013218. Springer (2014)","DOI":"10.1007\/978-3-319-11936-6_15"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: POPL. pp. 14\u201326. ACM (2001)","DOI":"10.1145\/360204.375719"},{"key":"3_CR30","unstructured":"Iverson, K.E.: A Programming Language. John Wiley & Sons, Inc., USA (1962)"},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: Verifast: A powerful, sound, predictable, fast verifier for C and java. In: NASA Formal Methods. Lecture Notes in Computer Science, vol.\u00a06617, pp. 41\u201355. Springer (2011)","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Jung, R., Krebbers, R., Jourdan, J., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, \u00a0e20 (2018)","DOI":"10.1017\/S0956796818000151"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Kaminski, B.L., Katoen, J.P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM 65(5) (2018)","DOI":"10.1145\/3208102"},{"key":"3_CR34","unstructured":"Kaminski, B.L.: Advanced weakest precondition calculi for probabilistic programs. Ph.D. thesis, RWTH Aachen University, Germany (2019)"},{"key":"3_CR35","doi-asserted-by":"crossref","unstructured":"Katelaan, J., Matheja, C., Zuleger, F.: Effective entailment checking for separation logic with inductive definitions. In: TACAS (2). Lecture Notes in Computer Science, vol. 11428, pp. 319\u2013336. Springer (2019)","DOI":"10.1007\/978-3-030-17465-1_18"},{"key":"3_CR36","doi-asserted-by":"crossref","unstructured":"Katoen, J., McIver, A., Meinicke, L., Morgan, C.C.: Linear-invariant generation for probabilistic programs: - automated support for proof-based methods. In: SAS. Lecture Notes in Computer Science, vol.\u00a06337, pp. 390\u2013406. Springer (2010)","DOI":"10.1007\/978-3-642-15769-1_24"},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Semantics of probabilistic programs. In: FOCS. pp. 101\u2013114. IEEE Computer Society (1979)","DOI":"10.1109\/SFCS.1979.38"},{"key":"3_CR38","doi-asserted-by":"crossref","unstructured":"Kozen, D.: A probabilistic PDL. In: STOC. pp. 291\u2013297. ACM (1983)","DOI":"10.1145\/800061.808758"},{"key":"3_CR39","unstructured":"Matheja, C.: Automated reasoning and randomization in separation logic. Ph.D. thesis, RWTH Aachen University, Germany (2020)"},{"key":"3_CR40","unstructured":"Matheja, C., Pagel, J., Zuleger, F.: Complete entailment checking for separation logic with inductive definitions. CoRR abs\/2002.01202 (2020)"},{"key":"3_CR41","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science, Springer (2005).","DOI":"10.1145\/1059816.1059824"},{"key":"3_CR42","doi-asserted-by":"crossref","unstructured":"Mitzenmacher, M., Upfal, E.: Probability and Computing: Randomized Algorithms and Probabilistic Analysis. Cambridge University Press (2005)","DOI":"10.1017\/CBO9780511813603"},{"key":"3_CR43","doi-asserted-by":"crossref","unstructured":"Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Trans. Program. Lang. Syst. 18(3), 325\u2013353 (may 1996)","DOI":"10.1145\/229542.229547"},{"key":"3_CR44","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: A verification infrastructure for permission-based reasoning. In: Dependable Software Systems Engineering, NATO Science for Peace and Security Series - D: Information and Communication Security, vol.\u00a050, pp. 104\u2013125. IOS Press (2017)"},{"key":"3_CR45","doi-asserted-by":"crossref","unstructured":"Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: Resource analysis for probabilistic programs. SIGPLAN Not. 53(4), 496\u2013512 (2018)","DOI":"10.1145\/3296979.3192394"},{"key":"3_CR46","doi-asserted-by":"crossref","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating separation logic using SMT. In: CAV. Lecture Notes in Computer Science, vol.\u00a08044, pp. 773\u2013789. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_54"},{"key":"3_CR47","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Iosif, R., Serban, C., King, T.: A decision procedure for separation logic in SMT. In: ATVA. Lecture Notes in Computer Science, vol.\u00a09938, pp. 244\u2013261 (2016)","DOI":"10.1007\/978-3-319-46520-3_16"},{"key":"3_CR48","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS. pp. 55\u201374. IEEE Computer Society (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"3_CR49","doi-asserted-by":"crossref","unstructured":"Saheb-Djahromi, N.: Probabilistic lcf. In: Winkowski, J. (ed.) Mathematical Foundations of Computer Science 1978. pp. 442\u2013451. Springer, Berlin, Heidelberg (1978)","DOI":"10.1007\/3-540-08921-7_92"},{"key":"3_CR50","doi-asserted-by":"crossref","unstructured":"Ta, Q., Le, T.C., Khoo, S., Chin, W.: Automated lemma synthesis in symbolic-heap separation logic. Proc. ACM Program. Lang. 2(POPL), 9:1\u20139:29 (2018)","DOI":"10.1145\/3158097"},{"key":"3_CR51","doi-asserted-by":"crossref","unstructured":"Tassarotti, J., Harper, R.: A separation logic for concurrent randomized programs. Proc. ACM Program. Lang. 3(POPL), 64:1\u201364:30 (2019)","DOI":"10.1145\/3290377"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99336-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T05:07:35Z","timestamp":1731647255000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99336-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030993351","9783030993368"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99336-8_3","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":"29 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","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":"5 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/esop","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":"64","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":"21","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":"33% - 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.5","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":"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)"}}]}}