{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:03:06Z","timestamp":1784199786451,"version":"3.55.0"},"reference-count":79,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","funder":[{"name":"ANR","award":["ANR-22-CE39-0014-03"],"award-info":[{"award-number":["ANR-22-CE39-0014-03"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>\n                    We introduce a new family of abstractions based on a data structure that we call\n                    <jats:italic toggle=\"yes\">labeled union-find<\/jats:italic>\n                    , an extension of the classic efficient union-find data structure where edges carry labels. These labels have a composition operation that obey the group axioms. Like union-find, the labeled version can efficiently compute the transitive closure of a relation, but it is not limited to equivalence relations; it can represent any injective transformation between equivalence classes, which includes two-variables per equality (TVPE) constraints of the form\n                    <jats:italic toggle=\"yes\">y<\/jats:italic>\n                    =\n                    <jats:italic toggle=\"yes\">a<\/jats:italic>\n                    \u00d7 +\n                    <jats:italic toggle=\"yes\">b<\/jats:italic>\n                    . Using abstract interpretation theory, we study the properties deriving from the use of abstract relations as labels, and the combination of labeled union-find with other representations of constraints, allowing both improvements in precision and simplification of existing constraints. Due to its efficiency, the labeled union-find abstractions could find many uses; we use it in two use cases, program analysis based on abstract interpretation and constraint solving for SMT, with encouraging preliminary results.\n                  <\/jats:p>","DOI":"10.1145\/3729298","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"1194-1219","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Relational Abstractions Based on Labeled Union-Find"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4328-6753","authenticated-orcid":false,"given":"Dorian","family":"Lesbre","sequence":"first","affiliation":[{"name":"Universit\u00e9 Paris-Saclay - CEA LIST, Palaiseau, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1081-0467","authenticated-orcid":false,"given":"Matthieu","family":"Lemerre","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay - CEA LIST, Palaiseau, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7909-0413","authenticated-orcid":false,"given":"Hichem Rami","family":"Ait-El-Hara","sequence":"additional","affiliation":[{"name":"OCamlPro, Paris, France"},{"name":"Universit\u00e9 Paris-Saclay - CEA LIST, Palaiseau, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6756-0788","authenticated-orcid":false,"given":"Fran\u00e7ois","family":"Bobot","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay - CEA LIST, Palaiseau, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.29007\/75tl"},{"key":"e_1_3_2_3_1","first-page":"64","volume-title":"Proceedings of the 22nd International Workshop on Satisfiability Modulo Theories (CEUR Workshop Proceedings, Vol. 3725)","author":"Ait-El-Hara Hichem Rami","year":"2024","unstructured":"Hichem Rami Ait-El-Hara, Fran\u00e7ois Bobot, and Guillaume Bury. 2024b. An SMT Theory for n-Indexed Sequences. In Proceedings of the 22nd International Workshop on Satisfiability Modulo Theories (CEUR Workshop Proceedings, Vol. 3725), Giles Reger and Yoni Zohar (Eds.). CEUR, Montreal, Canada, 64\u201374. https:\/\/ceur-ws.org\/Vol-3725\/#short13"},{"key":"e_1_3_2_4_1","volume-title":"The static single information form. Master\u2019s thesis","author":"Scott Ananian C","year":"2001","unstructured":"C Scott Ananian. 2001. The static single information form. Master\u2019s thesis. Massachusetts Institute of Technology. https:\/\/dspace.mit.edu\/bitstream\/handle\/1721.1\/86578\/48072795-MIT.pdf"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","unstructured":"Bengt Aspvall and Yossi Shiloach. 1980. A fast algorithm for solving systems of linear equations with two variables per equation Vol. 34. 117\u2013124. doi:10.1016\/0024-3795(80)90162-7","DOI":"10.1016\/0024-3795(80)90162-7"},{"key":"e_1_3_2_6_1","volume-title":"Data-Flow Analysis for Constraint Logic-Based Languages. Ph.D. Dissertation","author":"Bagnara Roberto","year":"1998","unstructured":"Roberto Bagnara. 1998. Data-Flow Analysis for Constraint Logic-Based Languages. Ph.D. Dissertation. Universita di Pisa."},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/646821.706603"},{"key":"e_1_3_2_8_1","unstructured":"Clack W. Barrett Pascal Fontaine and Cesare Tinelli. 2016. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/341176.341208"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","unstructured":"Dirk Beyer. 2024. SV-Benchmarks: Benchmark Set for Software Verification (SV-COMP 2024). doi:10.5281\/zenodo.10669723","DOI":"10.5281\/zenodo.10669723"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349342"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2180887.2180898"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74970-7_56"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_11"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-59776-8_1"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.04.080"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","unstructured":"Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL \u201977. 238\u2013252. doi:10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77505-8_23"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_25"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89812-2_7"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511609886.014"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/364099.364331"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3457885"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689609.3689994"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47764-0_20"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611973402.75"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1080\/00207168908803778"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0032748"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10703-006-0013-2"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53413-7_12"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2017.02.004"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571258"},{"key":"e_1_3_2_37_1","volume-title":"NSAD 24","author":"Lemerre Matthieu","year":"2024","unstructured":"Matthieu Lemerre and Dorian Lesbre. 2024. Labeled union-find for constraint factorization. In NSAD 24. Pasadena, United States. https:\/\/cea.hal.science\/cea-04996700"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/357062.357071"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656392"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","unstructured":"Dorian Lesbre Matthieu Lemerre Hichem Rami Ait-El-Hara and Fran\u00e7ois Bobot. 2025a. Artifact for paper \"Relational Abstractions Based on Labeled Union-Find\". doi:10.5281\/zenodo.15261356","DOI":"10.5281\/zenodo.15261356"},{"key":"e_1_3_2_41_1","doi-asserted-by":"crossref","unstructured":"Dorian Lesbre Matthieu Lemerre Hichem Rami Ait-El-Hara and Fran\u00e7ois Bobot. 2025b. Relational Abstractions Based on Labeled Union-Find (with appendices). Technical Report. https:\/\/hal.science\/hal-05029216","DOI":"10.1145\/3729298"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1363686.1363736"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(77)90007-8"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33558-7_39"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44978-7_10"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45789-5_11"},{"key":"e_1_3_2_47_1","volume-title":"Weakly relational numerical abstract domains. Ph. D. Dissertation","author":"Min\u00e9 Antoine","year":"2004","unstructured":"Antoine Min\u00e9. 2004. Weakly relational numerical abstract domains. Ph. D. Dissertation. \u00c9cole Polytechnique. http:\/\/www.di.ens.fr\/~mine\/these\/these-color.pdf."},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/WCRE.2001.957836"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.29007\/b63g"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000034"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-94583-1_10"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27836-8_85"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","unstructured":"Patrick Nappa David Zhao Pavle Subotic and Bernhard Scholz. 2019. Fast Parallel Equivalence Relations in a Datalog Compiler. In PACT 2019.IEEE 82\u201396. doi:10.1109\/PACT.2019.00015","DOI":"10.1109\/PACT.2019.00015"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660205"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_33"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854038.2854050"},{"key":"e_1_3_2_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90043-0"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13193-6_35"},{"key":"e_1_3_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69738-1_20"},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","unstructured":"Mathias Preiner Hans-J\u00f6rg Schurr Clark Barrett Pascal Fontaine Aina Niemetz and Cesare Tinelli. 2024. SMT-LIB release 2024 (non-incremental benchmarks). doi:10.5281\/zenodo.11061097","DOI":"10.5281\/zenodo.11061097"},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_3"},{"key":"e_1_3_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/1113830.1113833"},{"key":"e_1_3_2_63_1","doi-asserted-by":"publisher","unstructured":"Barry K Rosen Mark N Wegman and F Kenneth Zadeck. 1988. Global value numbers and redundant computations. In 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 1988). 12\u201327. doi:10.1145\/73560.73562","DOI":"10.1145\/73560.73562"},{"key":"e_1_3_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622840"},{"key":"e_1_3_2_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30044-8_2"},{"key":"e_1_3_2_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-44245-2_21"},{"key":"e_1_3_2_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-023-09682-2"},{"key":"e_1_3_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/2422.322411"},{"key":"e_1_3_2_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-010-9062-8"},{"key":"e_1_3_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738000"},{"key":"e_1_3_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009885"},{"key":"e_1_3_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158143"},{"key":"e_1_3_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237727"},{"key":"e_1_3_2_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/321879.321884"},{"key":"e_1_3_2_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/322154.322161"},{"key":"e_1_3_2_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/62.2160"},{"key":"e_1_3_2_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54807-9_2"},{"key":"e_1_3_2_78_1","doi-asserted-by":"publisher","unstructured":"Arnaud Venet and Guillaume P. Brat. 2004. Precise and efficient static array bound checking for large embedded C programs. In PLDI \u201904. 231\u2013242. doi:10.1145\/996841.996869","DOI":"10.1145\/996841.996869"},{"key":"e_1_3_2_79_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO53902.2022.9741267"},{"key":"e_1_3_2_80_1","unstructured":"Philip Zucker. 2022. https:\/\/www.philipzucker.com\/union-find-groupoid\/. Accessed 2025-03-10."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729298","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:03:05Z","timestamp":1784196185000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729298"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":79,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729298"],"URL":"https:\/\/doi.org\/10.1145\/3729298","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}