{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T23:03:32Z","timestamp":1784675012133,"version":"3.55.0"},"publisher-location":"Cham","reference-count":56,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308192","type":"print"},{"value":"9783031308208","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,4,20]],"date-time":"2023-04-20T00:00:00Z","timestamp":1681948800000},"content-version":"vor","delay-in-days":109,"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>Essential tasks for the verification of probabilistic programs include bounding expected outcomes and proving termination in finite expected runtime. We contribute a simple yet effective <jats:italic>inductive synthesis<\/jats:italic> approach for proving such <jats:italic>quantitative reachability properties<\/jats:italic> by generating <jats:italic>inductive invariants<\/jats:italic> on <jats:italic>source-code level<\/jats:italic>. Our implementation shows promise: It finds invariants for (in)finite-state programs, can beat state-of-the-art probabilistic model checkers, and is competitive with modern tools dedicated to invariant synthesis and expected runtime reasoning.<\/jats:p>","DOI":"10.1007\/978-3-031-30820-8_25","type":"book-chapter","created":{"date-parts":[[2023,4,19]],"date-time":"2023-04-19T19:02:36Z","timestamp":1681930956000},"page":"410-429","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":32,"title":["Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8705-2564","authenticated-orcid":false,"given":"Kevin","family":"Batz","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9663-7441","authenticated-orcid":false,"given":"Mingshuai","family":"Chen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0978-8466","authenticated-orcid":false,"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5185-2324","authenticated-orcid":false,"given":"Benjamin Lucien","family":"Kaminski","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9151-0441","authenticated-orcid":false,"given":"Christoph","family":"Matheja","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,4,20]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"Abate, A., Giacobbe, M., Roy, D.: Learning probabilistic termination proofs. In: CAV (2). Lecture Notes in Computer Science, vol. 12760, pp. 3\u201326. Springer (2021)","DOI":"10.1007\/978-3-030-81688-9_1"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Agrawal, S., Chatterjee, K., Novotn\u00fd, P.: Lexicographic ranking supermartingales. PACMPL 2(POPL), 34:1\u201334:32 (2018)","DOI":"10.1145\/3158122"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"de\u00a0Alfaro, L., Kwiatkowska, M.Z., Norman, G., Parker, D., Segala, R.: Symbolic model checking of probabilistic processes using MTBDDs and the Kronecker representation. In: TACAS. Lecture Notes in Computer Science, vol.\u00a01785, pp. 395\u2013410. Springer (2000)","DOI":"10.1007\/3-540-46419-0_27"},{"key":"25_CR4","unstructured":"Alur, R., Bod\u00edk, R., Dallal, E., Fisman, D., Garg, P., Juniwal, G., Kress-Gazit, H., Madhusudan, P., Martin, M.M.K., Raghothaman, M., Saha, S., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Dependable Software Systems Engineering, vol.\u00a040, pp. 1\u201325. IOS Press (2015)"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Andriushchenko, R., Ceska, M., Junges, S., Katoen, J.: Inductive synthesis for probabilistic programs reaches new horizons. In: TACAS (1). Lecture Notes in Computer Science, vol. 12651, pp. 191\u2013209. Springer (2021)","DOI":"10.1007\/978-3-030-72016-2_11"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Baier, C., Clarke, E.M., Hartonas-Garmhausen, V., Kwiatkowska, M.Z., Ryan, M.: Symbolic model checking for probabilistic processes. In: ICALP. Lecture Notes in Computer Science, vol.\u00a01256, pp. 430\u2013440. Springer (1997)","DOI":"10.1007\/3-540-63165-8_199"},{"key":"25_CR7","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press (2008)"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Baier, C., Klein, J., Leuschner, L., Parker, D., Wunderlich, S.: Ensuring the reliability of your model checker: Interval iteration for Markov decision processes. In: CAV (1). Lecture Notes in Computer Science, vol. 10426, pp. 160\u2013180. Springer (2017)","DOI":"10.1007\/978-3-319-63387-9_8"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Bao, J., Trivedi, N., Pathak, D., Hsu, J., Roy, S.: Data-driven invariant learning for probabilistic programs. In: CAV (1). Lecture Notes in Computer Science, vol. 13371, pp. 33\u201354. Springer (2022)","DOI":"10.1007\/978-3-031-13185-1_3"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Barthe, G., Espitau, T., Fioriti, L.M.F., Hsu, J.: Synthesizing probabilistic invariants via Doob\u2019s decomposition. In: CAV (1). Lecture Notes in Computer Science, vol.\u00a09779, pp. 43\u201361. Springer (2016)","DOI":"10.1007\/978-3-319-41528-4_3"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Kov\u00e1cs, L., Stankovic, M.: Automatic generation of moment-based invariants for prob-solvable loops. In: ATVA. Lecture Notes in Computer Science, vol. 11781, pp. 255\u2013276. Springer (2019)","DOI":"10.1007\/978-3-030-31784-3_15"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Batz, K., Chen, M., Junges, S., Kaminski, B.L., Katoen, J., Matheja, C.: Probabilistic program verification via inductive synthesis of inductive invariants. CoRR abs\/2205.06152 (2022)","DOI":"10.1007\/978-3-031-30820-8_25"},{"key":"25_CR13","doi-asserted-by":"publisher","unstructured":"Batz, K., Chen, M., Junges, S., Kaminski, B.L., Katoen, J., Matheja, C.: cegispro2: Artifact for paper \"probabilistic program verification via inductive synthesis of inductive invariants\" (2023). https:\/\/doi.org\/10.5281\/zenodo.7507921","DOI":"10.5281\/zenodo.7507921"},{"key":"25_CR14","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":"25_CR15","doi-asserted-by":"crossref","unstructured":"Batz, K., Junges, S., Kaminski, B.L., Katoen, J., Matheja, C., Schr\u00f6er, P.: PrIC3: Property directed reachability for MDPs. In: CAV (2). Lecture Notes in Computer Science, vol. 12225, pp. 512\u2013538. Springer (2020)","DOI":"10.1007\/978-3-030-53291-8_27"},{"key":"25_CR16","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":"25_CR17","unstructured":"Belle, V., Passerini, A., van den Broeck, G.: Probabilistic inference in hybrid domains by weighted model integration. In: IJCAI. pp. 2770\u20132776. AAAI Press (2015)"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"Ceska, M., Hensel, C., Junges, S., Katoen, J.: Counterexample-guided inductive synthesis for probabilistic systems. Formal Aspects Comput. 33(4-5), 637\u2013667 (2021)","DOI":"10.1007\/s00165-021-00547-2"},{"key":"25_CR19","doi-asserted-by":"crossref","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: CAV. Lecture Notes in Computer Science, vol.\u00a08044, pp. 511\u2013526. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Chakarov, A., Voronin, Y., Sankaranarayanan, S.: Deductive proofs of almost sure persistence and recurrence properties. In: TACAS. Lecture Notes in Computer Science, vol.\u00a09636, pp. 260\u2013279. Springer (2016)","DOI":"10.1007\/978-3-662-49674-9_15"},{"key":"25_CR21","unstructured":"Chakraborty, S., Fried, D., Meel, K.S., Vardi, M.Y.: From weighted to unweighted model counting. In: IJCAI. pp. 689\u2013695. AAAI Press (2015)"},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Meel, K.S., Mistry, R., Vardi, M.Y.: Approximate probabilistic inference via word-level counting. In: AAAI. pp. 3218\u20133224. AAAI Press (2016)","DOI":"10.1609\/aaai.v30i1.10416"},{"key":"25_CR23","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through Positivstellensatz\u2019s. In: CAV (1). Lecture Notes in Computer Science, vol.\u00a09779, pp. 3\u201322. Springer (2016)","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"25_CR24","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Novotn\u00fd, P., Zikelic, D.: Stochastic invariants for probabilistic termination. In: POPL. pp. 145\u2013160. ACM (2017)","DOI":"10.1145\/3093333.3009873"},{"key":"25_CR25","doi-asserted-by":"crossref","unstructured":"Chen, M., Katoen, J., Klinkenberg, L., Winkler, T.: Does a program yield the right distribution? Verifying probabilistic programs via generating functions. In: CAV (1). Lecture Notes in Computer Science, vol. 13371, pp. 79\u2013101. Springer (2022)","DOI":"10.1007\/978-3-031-13185-1_5"},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"Chen, Y., Hong, C., Wang, B., Zhang, L.: Counterexample-guided polynomial loop invariant generation by Lagrange interpolation. In: CAV (1). Lecture Notes in Computer Science, vol.\u00a09206, pp. 658\u2013674. Springer (2015)","DOI":"10.1007\/978-3-319-21690-4_44"},{"key":"25_CR27","doi-asserted-by":"crossref","unstructured":"Chistikov, D., Dimitrova, R., Majumdar, R.: Approximate counting in SMT and value estimation for probabilistic programs. Acta Informatica 54(8), 729\u2013764 (2017)","DOI":"10.1007\/s00236-017-0297-2"},{"key":"25_CR28","doi-asserted-by":"crossref","unstructured":"D\u2019Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reachability analysis of probabilistic systems by successive refinements. In: PAPM-PROBMIV. Lecture Notes in Computer Science, vol.\u00a02165, pp. 39\u201356. Springer (2001)","DOI":"10.1007\/3-540-44804-7_3"},{"key":"25_CR29","doi-asserted-by":"crossref","unstructured":"Fedyukovich, G., Bod\u00edk, R.: Accelerating syntax-guided invariant synthesis. In: TACAS (1). Lecture Notes in Computer Science, vol. 10805, pp. 251\u2013269. Springer (2018)","DOI":"10.1007\/978-3-319-89960-2_14"},{"key":"25_CR30","doi-asserted-by":"crossref","unstructured":"Feng, Y., Zhang, L., Jansen, D.N., Zhan, N., Xia, B.: Finding polynomial loop invariants for probabilistic programs. In: ATVA. Lecture Notes in Computer Science, vol. 10482, pp. 400\u2013416. Springer (2017)","DOI":"10.1007\/978-3-319-68167-2_26"},{"key":"25_CR31","doi-asserted-by":"crossref","unstructured":"Fioriti, L.M.F., Hermanns, H.: Probabilistic termination: Soundness, completeness, and compositionality. In: POPL. pp. 489\u2013501. ACM (2015)","DOI":"10.1145\/2775051.2677001"},{"key":"25_CR32","doi-asserted-by":"crossref","unstructured":"Fu, H., Chatterjee, K.: Termination of nondeterministic probabilistic programs. In: VMCAI. Lecture Notes in Computer Science, vol. 11388, pp. 468\u2013490. Springer (2019)","DOI":"10.1007\/978-3-030-11245-5_22"},{"key":"25_CR33","doi-asserted-by":"crossref","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: ICE: A robust framework for learning invariants. In: CAV. Lecture Notes in Computer Science, vol.\u00a08559, pp. 69\u201387. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"25_CR34","unstructured":"Gario, M., Micheli, A.: PySMT: A solver-agnostic library for fast prototyping of SMT-based algorithms. In: SMT Workshop (2015)"},{"key":"25_CR35","doi-asserted-by":"crossref","unstructured":"Gehr, T., Misailovic, S., Vechev, M.T.: PSI: Exact symbolic inference for probabilistic programs. In: CAV (1). Lecture Notes in Computer Science, vol.\u00a09779, pp. 62\u201383. Springer (2016)","DOI":"10.1007\/978-3-319-41528-4_4"},{"key":"25_CR36","doi-asserted-by":"crossref","unstructured":"Hark, M., Kaminski, B.L., Giesl, J., Katoen, J.: Aiming low is harder: Induction for lower bounds in probabilistic program verification. Proc. ACM Program. Lang. 4(POPL), 37:1\u201337:28 (2020)","DOI":"10.1145\/3371105"},{"key":"25_CR37","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Kaminski, B.L.: Optimistic value iteration. In: CAV (2). Lecture Notes in Computer Science, vol. 12225, pp. 488\u2013511. Springer (2020)","DOI":"10.1007\/978-3-030-53291-8_26"},{"key":"25_CR38","doi-asserted-by":"crossref","unstructured":"Helmink, L., Sellink, M.P.A., Vaandrager, F.W.: Proof-checking a data link protocol. In: TYPES. Lecture Notes in Computer Science, vol.\u00a0806, pp. 127\u2013165. Springer (1993)","DOI":"10.1007\/3-540-58085-9_75"},{"key":"25_CR39","doi-asserted-by":"crossref","unstructured":"Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589\u2013610 (2022)","DOI":"10.1007\/s10009-021-00633-z"},{"key":"25_CR40","doi-asserted-by":"crossref","unstructured":"Holtzen, S., Junges, S., Vazquez-Chanlatte, M., Millstein, T.D., Seshia, S.A., van den Broeck, G.: Model checking finite-horizon Markov chains with probabilistic inference. In: CAV (2). Lecture Notes in Computer Science, vol. 12760, pp. 577\u2013601. Springer (2021)","DOI":"10.1007\/978-3-030-81688-9_27"},{"key":"25_CR41","doi-asserted-by":"crossref","unstructured":"Holtzen, S., van den Broeck, G., Millstein, T.D.: Scaling exact inference for discrete probabilistic programs. Proc. ACM Program. Lang. 4(OOPSLA), 140:1\u2013140:31 (2020)","DOI":"10.1145\/3428208"},{"key":"25_CR42","unstructured":"Kaminski, B.L.: Advanced Weakest Precondition Calculi for Probabilistic Programs. Ph.D. thesis, RWTH Aachen University, Germany (2019)"},{"key":"25_CR43","doi-asserted-by":"crossref","unstructured":"Kaminski, B.L., Katoen, J., Matheja, C.: On the hardness of analyzing probabilistic programs. Acta Inform. 56(3), 255\u2013285 (2019)","DOI":"10.1007\/s00236-018-0321-1"},{"key":"25_CR44","doi-asserted-by":"crossref","unstructured":"Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run-times of probabilistic programs. In: ESOP. Lecture Notes in Computer Science, vol.\u00a09632, pp. 364\u2013389. Springer (2016)","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"25_CR45","doi-asserted-by":"crossref","unstructured":"Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM 65(5), 30:1\u201330:68 (2018)","DOI":"10.1145\/3208102"},{"key":"25_CR46","doi-asserted-by":"crossref","unstructured":"Katoen, J., McIver, A., Meinicke, L., Morgan, 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":"25_CR47","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":"25_CR48","doi-asserted-by":"crossref","unstructured":"Moosbrugger, M., Bartocci, E., Katoen, J., Kov\u00e1cs, L.: Automated termination analysis of polynomial probabilistic programs. In: ESOP. Lecture Notes in Computer Science, vol. 12648, pp. 491\u2013518. Springer (2021)","DOI":"10.1007\/978-3-030-72019-3_18"},{"key":"25_CR49","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: TACAS. Lecture Notes in Computer Science, vol.\u00a04963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"25_CR50","doi-asserted-by":"crossref","unstructured":"Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: Resource analysis for probabilistic programs. In: PLDI. pp. 496\u2013512. ACM (2018)","DOI":"10.1145\/3296979.3192394"},{"key":"25_CR51","unstructured":"Park, D.: Fixpoint induction and proofs of program properties. Mach. Intell. 5 (1969)"},{"key":"25_CR52","doi-asserted-by":"crossref","unstructured":"Puterman, M.L.: Markov Decision Processes. Wiley Series in Probability and Statistics, Wiley (1994)","DOI":"10.1002\/9780470316887"},{"key":"25_CR53","doi-asserted-by":"crossref","unstructured":"Quatmann, T., Katoen, J.: Sound value iteration. In: CAV (1). Lecture Notes in Computer Science, vol. 10981, pp. 643\u2013661. Springer (2018)","DOI":"10.1007\/978-3-319-96145-3_37"},{"key":"25_CR54","doi-asserted-by":"crossref","unstructured":"Rabe, M.N., Wintersteiger, C.M., Kugler, H., Yordanov, B., Hamadi, Y.: Symbolic approximation of the bounded reachability probability in large Markov chains. In: QEST. Lecture Notes in Computer Science, vol.\u00a08657, pp. 388\u2013403. Springer (2014)","DOI":"10.1007\/978-3-319-10696-0_30"},{"key":"25_CR55","doi-asserted-by":"crossref","unstructured":"Takisaka, T., Oyabu, Y., Urabe, N., Hasuo, I.: Ranking and repulsing supermartingales for reachability in randomized programs. ACM Trans. Program. Lang. Syst. 43(2), 5:1\u20135:46 (2021)","DOI":"10.1145\/3450967"},{"key":"25_CR56","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J.\u00a0Math. 5(2), 285\u2013309 (1955)","DOI":"10.2140\/pjm.1955.5.285"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30820-8_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,2]],"date-time":"2023-08-02T11:06:14Z","timestamp":1690974374000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30820-8_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308192","9783031308208"],"references-count":56,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30820-8_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"20 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","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":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","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":"169","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":"56","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":"6","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","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)"}}]}}