{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T16:25:56Z","timestamp":1754151956280,"version":"3.41.2"},"publisher-location":"Cham","reference-count":55,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031986789"},{"type":"electronic","value":"9783031986796"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T00:00:00Z","timestamp":1753142400000},"content-version":"vor","delay-in-days":202,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We present , the first model checking tool for probabilistic Pushdown Automata (pPDA) supporting temporal logic specifications.  provides a user-friendly probabilistic modeling language with recursion that automatically translates into Probabilistic Operator Precedence Automata (pOPA). pOPA are a class of pPDA that can express all the behaviors of probabilistic programs: sampling, conditioning, recursive procedures, and nested inference queries. On pOPA,  can solve reachability queries as well as qualitative and quantitative model checking queries for specifications in Linear Temporal Logic (LTL) and a fragment of Precedence Oriented Temporal\u00a0Logic (POTL), a logic for context-free properties such as pre\/post-conditioning.<\/jats:p>","DOI":"10.1007\/978-3-031-98679-6_5","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T09:19:55Z","timestamp":1753089595000},"page":"105-121","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["POPACheck: A Model Checker for\u00a0Probabilistic Pushdown Automata"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2569-6238","authenticated-orcid":false,"given":"Francesco","family":"Pontiggia","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8004-6601","authenticated-orcid":false,"given":"Ezio","family":"Bartocci","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7742-9233","authenticated-orcid":false,"given":"Michele","family":"Chiari","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"5_CR1","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press (2008)"},{"key":"5_CR2","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/J.JCSS.2023.03.005","volume":"136","author":"C Baier","year":"2023","unstructured":"Baier, C., Kiefer, S., Klein, J., M\u00fcller, D., Worrell, J.: Markov chains and unambiguous automata. J. Comput. Syst. Sci. 136, 113\u2013134 (2023). https:\/\/doi.org\/10.1016\/J.JCSS.2023.03.005","journal-title":"J. Comput. Syst. Sci."},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Brozek, V., Holecek, J., Kucera, A.: Discounted properties of probabilistic pushdown automata. In: LPAR 2008. LNCS, vol.\u00a05330, pp. 230\u2013242. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-89439-1_17","DOI":"10.1007\/978-3-540-89439-1_17"},{"issue":"2","key":"5_CR4","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/s10703-012-0166-0","volume":"43","author":"T Br\u00e1zdil","year":"2013","unstructured":"Br\u00e1zdil, T., Esparza, J., Kiefer, S., Kucera, A.: Analyzing probabilistic pushdown automata. Formal Methods Syst. Des. 43(2), 124\u2013163 (2013). https:\/\/doi.org\/10.1007\/s10703-012-0166-0","journal-title":"Formal Methods Syst. Des."},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Esparza, J., Kucera, A.: Analysis and prediction of the long-run behavior of probabilistic sequential programs with recursion (extended abstract). In: FOCS 2005, pp. 521\u2013530. IEEE Computer Society (2005). https:\/\/doi.org\/10.1109\/SFCS.2005.19","DOI":"10.1109\/SFCS.2005.19"},{"issue":"1","key":"5_CR6","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1016\/J.JCSS.2014.06.005","volume":"81","author":"T Br\u00e1zdil","year":"2015","unstructured":"Br\u00e1zdil, T., Kiefer, S., Kucera, A., Varekov\u00e1, I.H.: Runtime analysis of probabilistic programs with unbounded recursion. J. Comput. Syst. Sci. 81(1), 288\u2013310 (2015). https:\/\/doi.org\/10.1016\/J.JCSS.2014.06.005","journal-title":"J. Comput. Syst. Sci."},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Canny, J.F.: Some algebraic and geometric computations in PSPACE. In: STOC 1988, pp. 460\u2013467. ACM (1988). https:\/\/doi.org\/10.1145\/62212.62257","DOI":"10.1145\/62212.62257"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Chiari, M., Mandrioli, D., Pontiggia, F., Pradella, M.: A model checker for operator precedence languages. ACM Trans. Program. Lang. Syst. 45(3) (2023). https:\/\/doi.org\/10.1145\/3608443","DOI":"10.1145\/3608443"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-030-81688-9_18","volume-title":"Computer Aided Verification","author":"M Chiari","year":"2021","unstructured":"Chiari, M., Mandrioli, D., Pradella, M.: Model-checking structured context-free languages. In: Silva, A., Leino, K. (eds.) CAV 2021. LNCS, vol. 12760, pp. 387\u2013410. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_18"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Chiari, M., Mandrioli, D., Pradella, M.: A first-order complete temporal logic for structured context-free languages. Log. Methods Comput. Sci. 18:3 (2022).https:\/\/doi.org\/10.46298\/LMCS-18(3:11)2022","DOI":"10.46298\/LMCS-18(3:11)2022"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Couvreur, J., Saheb, N., Sutre, G.: An optimal automata approach to LTL model checking of probabilistic systems. In: LPAR 2003. LNCS, vol.\u00a02850, pp. 361\u2013375. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-39813-4_26","DOI":"10.1007\/978-3-540-39813-4_26"},{"issue":"6","key":"5_CR12","doi-asserted-by":"publisher","first-page":"2282","DOI":"10.1137\/090749591","volume":"39","author":"J Esparza","year":"2010","unstructured":"Esparza, J., Kiefer, S., Luttenberger, M.: Computing the least fixed point of positive polynomial systems. SIAM J. Comput. 39(6), 2282\u20132335 (2010). https:\/\/doi.org\/10.1137\/090749591","journal-title":"SIAM J. Comput."},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Esparza, J., Kret\u00ednsk\u00fd, J., Sickert, S.: A unified translation of linear temporal logic to $$\\omega $$-automata. J. ACM 67(6), 33:1\u201333:61 (2020). https:\/\/doi.org\/10.1145\/3417995","DOI":"10.1145\/3417995"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Esparza, J., Kucera, A., Mayr, R.: Model checking probabilistic pushdown automata. In: LICS 2004, pp. 12\u201321. IEEE Computer Society (2004). https:\/\/doi.org\/10.1109\/LICS.2004.1319596","DOI":"10.1109\/LICS.2004.1319596"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Etessami, K., Stewart, A., Yannakakis, M.: Polynomial time algorithms for multi-type branching processes and stochastic context-free grammars. In: STOC 2012, pp. 579\u2013588. ACM (2012). https:\/\/doi.org\/10.1145\/2213977.2214030","DOI":"10.1145\/2213977.2214030"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Etessami, K., Yannakakis, M.: Algorithmic verification of recursive probabilistic state machines. In: TACAS 2005. LNCS, vol.\u00a03440, pp. 253\u2013270. Springer (2005). https:\/\/doi.org\/10.1007\/978-3-540-31980-1_17","DOI":"10.1007\/978-3-540-31980-1_17"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Etessami, K., Yannakakis, M.: Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. In: STACS 2005. LNCS, vol.\u00a03404, pp. 340\u2013352. Springer (2005). https:\/\/doi.org\/10.1007\/978-3-540-31856-9_28","DOI":"10.1007\/978-3-540-31856-9_28"},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"Etessami, K., Yannakakis, M.: Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. J. ACM 56(1), 1:1\u20131:66 (2009). https:\/\/doi.org\/10.1145\/1462153.1462154","DOI":"10.1145\/1462153.1462154"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"Etessami, K., Yannakakis, M.: Model checking of recursive probabilistic systems. ACM Trans. Comput. Log. 13(2), 12:1\u201312:40 (2012). https:\/\/doi.org\/10.1145\/2159531.2159534","DOI":"10.1145\/2159531.2159534"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Etessami, K., Yannakakis, M.: Recursive Markov decision processes and recursive stochastic games. J. ACM 62(2), 11:1\u201311:69 (2015). https:\/\/doi.org\/10.1145\/2699431","DOI":"10.1145\/2699431"},{"key":"5_CR21","unstructured":"Evans, O., Stuhlm\u00fcller, A., Salvatier, J., Filan, D.: Modeling agents with probabilistic programs (2017). http:\/\/agentmodels.org"},{"issue":"3","key":"5_CR22","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1145\/321172.321179","volume":"10","author":"RW Floyd","year":"1963","unstructured":"Floyd, R.W.: Syntactic analysis and operator precedence. J. ACM 10(3), 316\u2013333 (1963). https:\/\/doi.org\/10.1145\/321172.321179","journal-title":"J. ACM"},{"issue":"7553","key":"5_CR23","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1038\/NATURE14541","volume":"521","author":"Z Ghahramani","year":"2015","unstructured":"Ghahramani, Z.: Probabilistic machine learning and artificial intelligence. Nat. 521(7553), 452\u2013459 (2015). https:\/\/doi.org\/10.1038\/NATURE14541","journal-title":"Nat."},{"key":"5_CR24","unstructured":"Goodman, N.D., Mansinghka, V.K., Roy, D.M., Bonawitz, K.A., Tenenbaum, J.B.: Church: a language for generative models. In: UAI 2008, pp. 220\u2013229. AUAI Press (2008)"},{"key":"5_CR25","unstructured":"Goodman, N.D., Tenenbaum, J.B., The ProbMods contributors: probabilistic models of cognition. http:\/\/probmods.org\/v2 (2016). Accessed 22 May 2025"},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: FOSE 2014, pp. 167\u2013181. ACM (2014). https:\/\/doi.org\/10.1145\/2593882.2593900","DOI":"10.1145\/2593882.2593900"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Haccou, P., Jagers, P., Vatutin, V.A.: Branching Processes: Variation, Growth, and Extinction of Populations. Cambridge University Press (2005)","DOI":"10.1017\/CBO9780511629136"},{"key":"5_CR28","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/s10009-021-00633-z","DOI":"10.1007\/s10009-021-00633-z"},{"key":"5_CR29","doi-asserted-by":"publisher","unstructured":"Jacobs, J.: Paradoxes of probabilistic programming: and how to condition on events of measure zero with infinitesimal probabilities. ACM Program. Lang. 5(POPL), 1\u201326 (2021). https:\/\/doi.org\/10.1145\/3434339","DOI":"10.1145\/3434339"},{"issue":"3\/4","key":"5_CR30","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1145\/2429135.2429155","volume":"46","author":"D Jovanovic","year":"2012","unstructured":"Jovanovic, D., de Moura, L.: Solving non-linear arithmetic. ACM Commun. Comput. Algebra 46(3\/4), 104\u2013105 (2012). https:\/\/doi.org\/10.1145\/2429135.2429155","journal-title":"ACM Commun. Comput. Algebra"},{"key":"5_CR31","doi-asserted-by":"publisher","unstructured":"Kucera, A., Esparza, J., Mayr, R.: Model checking probabilistic pushdown automata. Log. Methods Comput. Sci. 2(1) (2006). https:\/\/doi.org\/10.2168\/LMCS-2(1:2)2006","DOI":"10.2168\/LMCS-2(1:2)2006"},{"key":"5_CR32","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: CAV 2011. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"5_CR33","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.cosrev.2017.12.001","volume":"27","author":"D Mandrioli","year":"2018","unstructured":"Mandrioli, D., Pradella, M.: Generalizing input-driven languages: theoretical and practical benefits. Comput. Sci. Rev. 27, 61\u201387 (2018). https:\/\/doi.org\/10.1016\/j.cosrev.2017.12.001","journal-title":"Comput. Sci. Rev."},{"key":"5_CR34","unstructured":"McConnell, J.: Analysis of Algorithms. Jones & Bartlett Publishers (2007)"},{"key":"5_CR35","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"5_CR36","doi-asserted-by":"publisher","unstructured":"Olmedo, F., Gretz, F., Jansen, N., Kaminski, B.L., Katoen, J., McIver, A.: Conditioning in probabilistic programming. ACM Trans. Program. Lang. Syst. 40(1), 4:1\u20134:50 (2018). https:\/\/doi.org\/10.1145\/3156018","DOI":"10.1145\/3156018"},{"key":"5_CR37","doi-asserted-by":"publisher","unstructured":"Olmedo, F., Kaminski, B.L., Katoen, J., Matheja, C.: Reasoning about recursive probabilistic programs. In: LICS 2016, pp. 672\u2013681. ACM (2016). https:\/\/doi.org\/10.1145\/2933575.2935317","DOI":"10.1145\/2933575.2935317"},{"key":"5_CR38","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS 1977, pp. 46\u201357. IEEE Computer Society (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"5_CR39","unstructured":"Pontiggia, F.: POMC. A model checking tool for operator precedence languages on omega-words. Master\u2019s thesis, Politecnico di Milano (2021). http:\/\/hdl.handle.net\/10589\/176028"},{"key":"5_CR40","unstructured":"Pontiggia, F., Bartocci, E., Chiari, M.: Model checking probabilistic operator precedence automata. CoRR (2024). https:\/\/doi.org\/10.48550\/arXiv.2404.03515"},{"key":"5_CR41","doi-asserted-by":"publisher","unstructured":"Pontiggia, F., Chiari, M., Pradella, M.: Verification of programs with exceptions through operator precedence automata. In: SEFM 2021. LNCS, vol. 13085, pp. 293\u2013311. Springer, Berlin, Heidelberg (2021). https:\/\/doi.org\/10.1007\/978-3-030-92124-8_17","DOI":"10.1007\/978-3-030-92124-8_17"},{"key":"5_CR42","unstructured":"Rainforth, T.: Nesting probabilistic programs. In: Globerson, A., Silva, R. (eds.) UAI 2018, pp. 249\u2013258. AUAI Press (2018). http:\/\/auai.org\/uai2018\/proceedings\/papers\/92.pdf"},{"issue":"3","key":"5_CR43","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/S0747-7171(10)80003-3","volume":"13","author":"J Renegar","year":"1992","unstructured":"Renegar, J.: On the computational complexity and geometry of the first-order theory of the reals, parts I-III. J. Symb. Comput. 13(3), 255\u2013352 (1992). https:\/\/doi.org\/10.1016\/S0747-7171(10)80003-3","journal-title":"J. Symb. Comput."},{"key":"5_CR44","unstructured":"Schelling, T.C.: The Strategy of Conflict. Harvard University Press (1980)"},{"key":"5_CR45","unstructured":"Scontras, G., Tessler, M.H., Franke, M.: Probabilistic language understanding: an introduction to the rational speech act framework. https:\/\/www.problang.org\/. Accessed 22 May 2025"},{"key":"5_CR46","unstructured":"Seaman, I.R., van\u00a0de Meent, J.W., Wingate, D.: Nested reasoning about autonomous agents using probabilistic programs (2020). https:\/\/arxiv.org\/abs\/1812.01569"},{"key":"5_CR47","doi-asserted-by":"publisher","unstructured":"Stewart, A., Etessami, K., Yannakakis, M.: Upper bounds for Newton\u2019s method on monotone polynomial systems, and P-time model checking of probabilistic one-counter automata. J. ACM 62(4), 30:1\u201330:33 (2015). https:\/\/doi.org\/10.1145\/2789208","DOI":"10.1145\/2789208"},{"key":"5_CR48","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1016\/J.COGSYS.2013.07.003","volume":"28","author":"A Stuhlm\u00fcller","year":"2014","unstructured":"Stuhlm\u00fcller, A., Goodman, N.D.: Reasoning about reasoning by nested conditioning: modeling theory of mind with probabilistic programs. Cogn. Syst. Res. 28, 80\u201399 (2014). https:\/\/doi.org\/10.1016\/J.COGSYS.2013.07.003","journal-title":"Cogn. Syst. Res."},{"issue":"1","key":"5_CR49","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/INCO.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994). https:\/\/doi.org\/10.1006\/INCO.1994.1092","journal-title":"Inf. Comput."},{"key":"5_CR50","doi-asserted-by":"publisher","unstructured":"Winkler, T., Gehnen, C., Katoen, J.: Model checking temporal properties of recursive probabilistic programs. In: FOSSACS 2022. LNCS, vol. 13242, pp. 449\u2013469. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99253-8_23","DOI":"10.1007\/978-3-030-99253-8_23"},{"key":"5_CR51","doi-asserted-by":"publisher","unstructured":"Winkler, T., Katoen, J.: Certificates for probabilistic pushdown automata via optimistic value iteration. In: TACAS 2023. LNCS, vol. 13994, pp. 391\u2013409. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_24","DOI":"10.1007\/978-3-031-30820-8_24"},{"key":"5_CR52","doi-asserted-by":"publisher","unstructured":"Winkler, T., Katoen, J.: On certificates, expected runtimes, and termination in probabilistic pushdown automata. In: LICS 2023, pp. 1\u201313 (2023). https:\/\/doi.org\/10.1109\/LICS56636.2023.10175714","DOI":"10.1109\/LICS56636.2023.10175714"},{"key":"5_CR53","doi-asserted-by":"publisher","unstructured":"Wojtczak, D., Etessami, K.: PReMo: An analyzer for probabilistic recursive models. In: TACAS 2007. LNCS, vol.\u00a04424, pp. 66\u201371. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_7","DOI":"10.1007\/978-3-540-71209-1_7"},{"key":"5_CR54","doi-asserted-by":"publisher","unstructured":"Yannakakis, M., Etessami, K.: Checking LTL properties of recursive Markov chains. In: QEST 2005, pp. 155\u2013165. IEEE (2005). https:\/\/doi.org\/10.1109\/QEST.2005.8","DOI":"10.1109\/QEST.2005.8"},{"key":"5_CR55","doi-asserted-by":"publisher","unstructured":"Zhang, Y., Amin, N.: Reasoning about \u201creasoning about reasoning\u201d: semantics and contextual equivalence for probabilistic programs with nested queries and recursion. ACM Program. Lang. 6(POPL), 1\u201328 (2022). https:\/\/doi.org\/10.1145\/3498677","DOI":"10.1145\/3498677"}],"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-98679-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T09:20:00Z","timestamp":1753089600000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98679-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986789","9783031986796"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98679-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"22 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors declare no competing interests for this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"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":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}