{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T16:10:52Z","timestamp":1746115852679,"version":"3.40.4"},"publisher-location":"Cham","reference-count":58,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031911170"},{"type":"electronic","value":"9783031911187"}],"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,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"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>Algorithmic versions of the Lov\u00e1sz Local Lemma (ALLLs), or rather, the Moser-Tardos algorithm and its variants, are impactful in both theory and practice. In this paper, we take the first step towards the goal of formally verifying ALLLs by applying programming language techniques. We propose two proof recipes, called loop truncation and resampling-table-based coupling, for bridging the gap between Hoare-style program logics and ALLLs\u2019 original informal proofs. We formally verify six existing important results related to ALLLs, and propose a new result which generalizes several existing results. Our proof recipes can also be used to verify general properties of other probabilistic programs in addition to ALLLs.<\/jats:p>","DOI":"10.1007\/978-3-031-91118-7_15","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:17:48Z","timestamp":1746001068000},"page":"379-407","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Verifying Algorithmic Versions of the Lov\u00e1sz Local Lemma"],"prefix":"10.1007","author":[{"given":"Rongen","family":"Lin","sequence":"first","affiliation":[]},{"given":"Hongjin","family":"Liang","sequence":"additional","affiliation":[]},{"given":"Xinyu","family":"Feng","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"15_CR1","doi-asserted-by":"publisher","unstructured":"Achlioptas, D., Gouleakis, T.: Algorithmic improvements of the Lov\u00e1sz local lemma via cluster expansion. In: FSTTCS 2012. pp. 16\u201323 (2012). https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2012.16","DOI":"10.4230\/LIPIcs.FSTTCS.2012.16"},{"key":"15_CR2","doi-asserted-by":"publisher","unstructured":"Anderson, E., Phillips, C., Sicker, D., Grunwald, D.: Optimization decomposition for scheduling and system configuration in wireless networks. IEEE\/ACM Trans. Netw. 22(1), 271\u2013284 (2014). https:\/\/doi.org\/10.1109\/TNET.2013.2289980","DOI":"10.1109\/TNET.2013.2289980"},{"key":"15_CR3","doi-asserted-by":"publisher","unstructured":"Barthe, G., Espitau, T., Gaboardi, M., Gr\u00e9goire, B., Hsu, J., Strub, P.Y.: An assertion-based program logic for probabilistic programs. In: ESOP 2018. pp. 117\u2013144 (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_5","DOI":"10.1007\/978-3-319-89884-1_5"},{"key":"15_CR4","doi-asserted-by":"publisher","unstructured":"Barthe, G., Espitau, T., Gr\u00e9goire, B., Hsu, J., Stefanesco, L., Strub, P.Y.: Relational reasoning via probabilistic coupling. In: LPAR 2015. p. 387\u2013401 (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_27","DOI":"10.1007\/978-3-662-48899-7_27"},{"key":"15_CR5","doi-asserted-by":"publisher","unstructured":"Barthe, G., Gaboardi, M., Gr\u00e9goire, B., Hsu, J., Strub, P.Y.: Proving differential privacy via probabilistic couplings. In: LICS 2016. p. 749\u2013758 (2016). https:\/\/doi.org\/10.1145\/2933575.2934554","DOI":"10.1145\/2933575.2934554"},{"key":"15_CR6","doi-asserted-by":"publisher","unstructured":"Barthe, G., Gr\u00e9goire, B., Zanella B\u00e9guelin, S.: Formal certification of code-based cryptographic proofs. In: POPL 2009. p. 90\u2013101 (2009). https:\/\/doi.org\/10.1145\/1480881.1480894","DOI":"10.1145\/1480881.1480894"},{"key":"15_CR7","doi-asserted-by":"publisher","unstructured":"Batz, K., Kaminski, B.L., Katoen, J.P., Matheja, C.: Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. Proc. ACM Program. Lang. 5(POPL), 1\u201330 (2021). https:\/\/doi.org\/10.1145\/3434320","DOI":"10.1145\/3434320"},{"key":"15_CR8","doi-asserted-by":"publisher","unstructured":"Bissacot, R., Fern\u00e1ndez, R., Procacci, A., Scoppola, B.: An improvement of the Lov\u00e1sz local lemma via cluster expansion. Comb. Probab. Comput. 20(5), 709\u2013719 (2011). https:\/\/doi.org\/10.1017\/S0963548311000253","DOI":"10.1017\/S0963548311000253"},{"key":"15_CR9","doi-asserted-by":"publisher","unstructured":"Boissonnat, J., Dyer, R., Ghosh, A.: A probabilistic approach to reducing algebraic complexity of delaunay triangulations. In: ESA 2015. pp. 595\u2013606 (2015). https:\/\/doi.org\/10.1007\/978-3-662-48350-3_50","DOI":"10.1007\/978-3-662-48350-3_50"},{"key":"15_CR10","doi-asserted-by":"publisher","unstructured":"Borgstr\u00f6m, J., Dal\u00a0Lago, U., Gordon, A.D., Szymczak, M.: A lambda-calculus foundation for universal probabilistic programming. In: ICFP 2016. pp. 33\u201346 (2016). https:\/\/doi.org\/10.1145\/2951913.2951942","DOI":"10.1145\/2951913.2951942"},{"key":"15_CR11","doi-asserted-by":"publisher","unstructured":"Bournez, O., Garnier, F.: Proving positive almost-sure termination. In: RTA 2005. pp. 323\u2013337 (2005). https:\/\/doi.org\/10.1007\/978-3-540-32033-3_24","DOI":"10.1007\/978-3-540-32033-3_24"},{"key":"15_CR12","doi-asserted-by":"publisher","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: CAV 2013. pp. 511\u2013526 (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"15_CR13","doi-asserted-by":"publisher","unstructured":"Chang, Y.J., He, Q., Li, W., Pettie, S., Uitto, J.: Distributed edge coloring and a special case of the constructive Lov\u00e1sz local lemma. ACM Trans. Algorithms 16(1), 8:1\u20138:51 (2020). https:\/\/doi.org\/10.1145\/3365004","DOI":"10.1145\/3365004"},{"key":"15_CR14","doi-asserted-by":"publisher","unstructured":"Chen, A., Harris, D.G., Srinivasan, A.: Partial resampling to approximate covering integer programs. Random Struct. Algorithms 58(1), 68\u201393 (2021). https:\/\/doi.org\/10.1002\/rsa.20964","DOI":"10.1002\/rsa.20964"},{"key":"15_CR15","doi-asserted-by":"publisher","unstructured":"Cheng, K., Haeupler, B., Li, X., Shahrasbi, A., Wu, K.: Synchronization strings: Highly efficient deterministic constructions over small alphabets. In: SODA 2019. pp. 2185\u20132204 (2019). https:\/\/doi.org\/10.1137\/1.9781611975482.132","DOI":"10.1137\/1.9781611975482.132"},{"key":"15_CR16","doi-asserted-by":"publisher","unstructured":"Chung, K.M., Pettie, S., Su, H.H.: Distributed algorithms for the Lov\u00e1sz local lemma and graph coloring. In: PODC 2014. p. 134\u2013143 (2014). https:\/\/doi.org\/10.1145\/2611462.2611465","DOI":"10.1145\/2611462.2611465"},{"key":"15_CR17","doi-asserted-by":"publisher","unstructured":"Culpepper, R., Cobb, A.: Contextual equivalence for probabilistic programs with continuous random variables and scoring. In: ESOP 2017. pp. 368\u2013392 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_14","DOI":"10.1007\/978-3-662-54434-1_14"},{"key":"15_CR18","doi-asserted-by":"publisher","unstructured":"Edmonds, C., Paulson, L.C.: Formal probabilistic methods for combinatorial structures using the Lov\u00e1sz local lemma. In: CPP 2024. pp. 132\u2013146 (2024). https:\/\/doi.org\/10.1145\/3636501.3636946","DOI":"10.1145\/3636501.3636946"},{"key":"15_CR19","unstructured":"Erd\u0151s, P., Lov\u00e1sz, L.: Problems and results on 3-chromatic hypergraphs and some related questions. Infinite and finite sets 10(2), 609\u2013627 (1975)"},{"key":"15_CR20","doi-asserted-by":"publisher","unstructured":"Erd\u0151s, P., Spencer, J.: Lopsided Lov\u00e1sz local lemma and latin transversals. Discrete Applied Mathematics 30(151-154), 10\u20131016 (1991). https:\/\/doi.org\/10.1016\/0166-218X(91)90040-4","DOI":"10.1016\/0166-218X(91)90040-4"},{"key":"15_CR21","unstructured":"Fan, W., Liang, H., Feng, X., Jiang, H.: A program logic for concurrent randomized programs in the oblivious adversary model. To appear in ESOP 2025."},{"key":"15_CR22","doi-asserted-by":"publisher","unstructured":"Feng, S., Chen, M., Su, H., Kaminski, B.L., Katoen, J., Zhan, N.: Lower bounds for possibly divergent probabilistic programs. Proc. ACM Program. Lang. 7(OOPSLA1), 696\u2013726 (2023). https:\/\/doi.org\/10.1145\/3586051","DOI":"10.1145\/3586051"},{"key":"15_CR23","doi-asserted-by":"publisher","unstructured":"Fern\u00e1ndez, M., Livieratos, J., Mart\u00edn, S.: Bounds and constructions of parent identifying schemes via the algorithmic version of the Lov\u00e1sz local lemma. IEEE Trans. Inf. Theory 69(11), 7049\u20137069 (2023). https:\/\/doi.org\/10.1109\/TIT.2023.3282452","DOI":"10.1109\/TIT.2023.3282452"},{"key":"15_CR24","doi-asserted-by":"publisher","unstructured":"Ferrer Fioriti, L.M., Hermanns, H.: Probabilistic termination: Soundness, completeness, and compositionality. In: POPL 2015. p. 489\u2013501 (2015). https:\/\/doi.org\/10.1145\/2676726.2677001","DOI":"10.1145\/2676726.2677001"},{"key":"15_CR25","doi-asserted-by":"publisher","unstructured":"Fischer, M., Ghaffari, M.: Sublogarithmic distributed algorithms for Lov\u00e1sz local lemma, and the complexity hierarchy. In: DISC 2017. pp. 18:1\u201318:16 (2017). https:\/\/doi.org\/10.4230\/LIPIcs.DISC.2017.18","DOI":"10.4230\/LIPIcs.DISC.2017.18"},{"key":"15_CR26","doi-asserted-by":"publisher","unstructured":"Gebauer, H., Szab\u00f3, T., Tardos, G.: The local lemma is asymptotically tight for SAT. J. ACM 63(5), 43:1\u201343:32 (2016). https:\/\/doi.org\/10.1145\/2975386","DOI":"10.1145\/2975386"},{"key":"15_CR27","doi-asserted-by":"publisher","unstructured":"Graf, A., Harris, D.G., Haxell, P.: Algorithms for weighted independent transversals and strong colouring. ACM Trans. Algorithms 18(1), 1:1\u20131:16 (2022). https:\/\/doi.org\/10.1145\/3474057","DOI":"10.1145\/3474057"},{"key":"15_CR28","doi-asserted-by":"publisher","unstructured":"Gregersen, S.O., Aguirre, A., Haselwarter, P.G., Tassarotti, J., Birkedal, L.: Asynchronous probabilistic couplings in higher-order separation logic. Proc. ACM Program. Lang. 8(POPL), 753\u2013784 (2024). https:\/\/doi.org\/10.1145\/3632868","DOI":"10.1145\/3632868"},{"key":"15_CR29","doi-asserted-by":"publisher","unstructured":"Guo, H., Jerrum, M., Liu, J.: Uniform sampling through the Lov\u00e1sz local lemma. J. ACM 66(3), 18:1\u201318:31 (2019). https:\/\/doi.org\/10.1145\/3310131","DOI":"10.1145\/3310131"},{"key":"15_CR30","doi-asserted-by":"publisher","unstructured":"Haeupler, B., Harris, D.G.: Parallel algorithms and concentration bounds for the Lov\u00e1sz local lemma via witness dags. ACM Trans. Algorithms 13(4), 53:1\u201353:25 (2017). https:\/\/doi.org\/10.1145\/3147211","DOI":"10.1145\/3147211"},{"key":"15_CR31","doi-asserted-by":"publisher","unstructured":"Haeupler, B., Saha, B., Srinivasan, A.: New constructive aspects of the Lov\u00e1sz local lemma. J. ACM 58(6), 28:1\u201328:28 (2011). https:\/\/doi.org\/10.1145\/2049697.2049702","DOI":"10.1145\/2049697.2049702"},{"key":"15_CR32","doi-asserted-by":"publisher","unstructured":"Harris, D.G.: New bounds for the Moser-Tardos distribution. Random Struct. Algorithms 57(1), 97\u2013131 (2020). https:\/\/doi.org\/10.1002\/rsa.20914","DOI":"10.1002\/rsa.20914"},{"key":"15_CR33","doi-asserted-by":"publisher","unstructured":"Harris, D.G., Srinivasan, A.: Constraint satisfaction, packet routing, and the Lov\u00e1sz local lemma. In: STOC 13. p. 685\u2013694 (2013). https:\/\/doi.org\/10.1145\/2488608.2488696","DOI":"10.1145\/2488608.2488696"},{"key":"15_CR34","doi-asserted-by":"publisher","unstructured":"Harris, D.G., Srinivasan, A.: A constructive algorithm for the Lov\u00e1sz local lemma on permutations. In: SODA 2014. pp. 907\u2013925 (2014). https:\/\/doi.org\/10.1137\/1.9781611973402.68","DOI":"10.1137\/1.9781611973402.68"},{"key":"15_CR35","doi-asserted-by":"publisher","unstructured":"Harris, D.G., Srinivasan, A.: Algorithmic and enumerative aspects of the Moser-Tardos distribution. ACM Trans. Algorithms 13(3), 33:1\u201333:40 (2017). https:\/\/doi.org\/10.1145\/3039869","DOI":"10.1145\/3039869"},{"key":"15_CR36","doi-asserted-by":"publisher","unstructured":"Harris, D.G., Srinivasan, A.: The Moser-Tardos framework with partial resampling. J. ACM 66(5), 36:1\u201336:45 (2019). https:\/\/doi.org\/10.1145\/3342222","DOI":"10.1145\/3342222"},{"key":"15_CR37","doi-asserted-by":"publisher","unstructured":"He, K., Li, Q., Sun, X.: Moser-Tardos algorithm: Beyond Shearer\u2019s bound. In: SODA 2023. pp. 3362\u20133387 (2023). https:\/\/doi.org\/10.1137\/1.9781611977554.CH129","DOI":"10.1137\/1.9781611977554.CH129"},{"key":"15_CR38","doi-asserted-by":"publisher","unstructured":"Huang, M., Fu, H., Chatterjee, K., Goharshady, A.K.: Modular verification for almost-sure termination of probabilistic programs. Proc. ACM Program. Lang. 3(OOPSLA), 129:1\u2013129:29 (2019). https:\/\/doi.org\/10.1145\/3360555","DOI":"10.1145\/3360555"},{"key":"15_CR39","doi-asserted-by":"publisher","unstructured":"Jiang, N., Gu, Y., Xue, Y.: Learning Markov random fields for combinatorial structures via sampling through Lov\u00e1sz local lemma. In: AAAI 2023. pp. 4016\u20134024 (2023). https:\/\/doi.org\/10.1609\/AAAI.V37I4.25516","DOI":"10.1609\/AAAI.V37I4.25516"},{"key":"15_CR40","doi-asserted-by":"publisher","unstructured":"Kaminski, B.L.: Advanced weakest precondition calculi for probabilistic programs. Ph.D. thesis, RWTH Aachen University, Germany (2019). https:\/\/doi.org\/10.18154\/RWTH-2019-01829","DOI":"10.18154\/RWTH-2019-01829"},{"key":"15_CR41","doi-asserted-by":"publisher","unstructured":"Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run-times of probabilistic programs. In: ESOP 2016. pp. 364\u2013389 (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_15","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"15_CR42","doi-asserted-by":"publisher","unstructured":"Kolipaka, K.B.R., Szegedy, M.: Moser and Tardos meet Lov\u00e1sz. In: STOC 2011. p. 235\u2013244 (2011). https:\/\/doi.org\/10.1145\/1993636.1993669","DOI":"10.1145\/1993636.1993669"},{"key":"15_CR43","doi-asserted-by":"publisher","unstructured":"Kolipaka, K.B.R., Szegedy, M., Xu, Y.: A sharper local lemma with improved applications. In: APPROX-RANDOM 2012. pp. 603\u2013614 (2012). https:\/\/doi.org\/10.1007\/978-3-642-32512-0_51","DOI":"10.1007\/978-3-642-32512-0_51"},{"key":"15_CR44","doi-asserted-by":"publisher","unstructured":"Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328\u2013350 (1981). https:\/\/doi.org\/10.1016\/0022-0000(81)90036-2","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"15_CR45","doi-asserted-by":"publisher","unstructured":"Kozen, D.: A probabilistic PDL. J. Comput. Syst. Sci. 30(2), 162\u2013178 (1985). https:\/\/doi.org\/10.1016\/0022-0000(85)90012-1","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"15_CR46","unstructured":"Lin, R., Liang, H., Feng, X.: Verifying algorithmic versions of the Lov\u00e1sz local lemma \u2013 technical report. https:\/\/plax-lab.github.io\/publications\/alll\/alll-tr.pdf (2024)"},{"key":"15_CR47","doi-asserted-by":"publisher","unstructured":"Majumdar, R., Sathiyanarayana, V.R.: Positive almost-sure termination: Complexity and proof rules. Proc. ACM Program. Lang. 8(POPL), 1089\u20131117 (2024). https:\/\/doi.org\/10.1145\/3632879","DOI":"10.1145\/3632879"},{"key":"15_CR48","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer (2005). https:\/\/doi.org\/10.1007\/B138392","DOI":"10.1007\/B138392"},{"key":"15_CR49","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.: A new proof rule for almost-sure termination. Proc. ACM Program. Lang. 2(POPL), 33:1\u201333:28 (2018). https:\/\/doi.org\/10.1145\/3158121","DOI":"10.1145\/3158121"},{"key":"15_CR50","doi-asserted-by":"publisher","unstructured":"Moser, R.A., Tardos, G.: A constructive proof of the general Lov\u00e1sz local lemma. J.\u00a0ACM 57(2), 11:1\u201311:15 (2010). https:\/\/doi.org\/10.1145\/1667053.1667060","DOI":"10.1145\/1667053.1667060"},{"key":"15_CR51","doi-asserted-by":"publisher","unstructured":"Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: Resource analysis for probabilistic programs. In: PLDI 2018. p. 496\u2013512 (2018). https:\/\/doi.org\/10.1145\/3192366.3192394","DOI":"10.1145\/3192366.3192394"},{"key":"15_CR52","doi-asserted-by":"publisher","unstructured":"Olmedo, F., Kaminski, B.L., Katoen, J.P., Matheja, C.: Reasoning about recursive probabilistic programs. In: LICS 2016. p. 672\u2013681 (2016). https:\/\/doi.org\/10.1145\/2933575.2935317","DOI":"10.1145\/2933575.2935317"},{"key":"15_CR53","doi-asserted-by":"publisher","unstructured":"Pegden, W.: An extension of the Moser-Tardos algorithmic local lemma. SIAM J. Discret. Math. 28(2), 911\u2013917 (2014). https:\/\/doi.org\/10.1137\/110828290","DOI":"10.1137\/110828290"},{"key":"15_CR54","doi-asserted-by":"publisher","unstructured":"Saeki, S.: A proof of the existence of infinite product probability measures. The American Mathematical Monthly 103(8), 682\u2013683 (1996). https:\/\/doi.org\/10.1080\/00029890.1996.12004804","DOI":"10.1080\/00029890.1996.12004804"},{"key":"15_CR55","doi-asserted-by":"publisher","unstructured":"Sarkar, K., Colbourn, C.J., Bonis, A.D., Vaccaro, U.: Partial covering arrays: Algorithms and asymptotics. Theory Comput. Syst. 62(6), 1470\u20131489 (2018). https:\/\/doi.org\/10.1007\/S00224-017-9782-9","DOI":"10.1007\/S00224-017-9782-9"},{"key":"15_CR56","doi-asserted-by":"publisher","unstructured":"Shearer, J.B.: On a problem of Spencer. Combinatorica 5, 241\u2013245 (1985). https:\/\/doi.org\/10.1007\/BF02579368","DOI":"10.1007\/BF02579368"},{"key":"15_CR57","doi-asserted-by":"publisher","unstructured":"Spencer, J.: Asymptotic lower bounds for Ramsey functions. Discrete Mathematics 20, 69\u201376 (1977). https:\/\/doi.org\/10.1016\/0012-365X(77)90044-9","DOI":"10.1016\/0012-365X(77)90044-9"},{"key":"15_CR58","unstructured":"Srinivasan, A.: Progress on algorithmic versions of the Lov\u00e1sz local lemma. https:\/\/www.ias.edu\/sites\/default\/files\/video\/Aravind.pdf (2013)"}],"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-031-91118-7_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:17:51Z","timestamp":1746001071000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-91118-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031911170","9783031911187"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-91118-7_15","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":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"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":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","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":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}