{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T14:13:50Z","timestamp":1784211230452,"version":"3.55.0"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>\n                    Static analyses play a fundamental role during compilation: they discover facts that are true in all executions of the code being compiled, and then these facts are used to justify optimizations and diagnostics. Each static analysis is based on a collection of\n                    <jats:italic toggle=\"yes\">abstract transformers<\/jats:italic>\n                    that provide abstract semantics for the concrete instructions that make up a program. It can be challenging to implement abstract transformers that are sound, precise, and efficient\u2014and in fact both LLVM and GCC have suffered from miscompilations caused by unsound abstract transformers. Moreover, even after more than 20 years of development, LLVM lacks abstract transformers for hundreds of instructions in its intermediate representation (IR).\n                  <\/jats:p>\n                  <jats:p>\n                    We developed\n                    <jats:monospace>NiceToMeetYou<\/jats:monospace>\n                    : a program synthesis framework for abstract transformers that are aimed at the kinds of non-relational integer abstract domains that are heavily used by today\u2019s production compilers. It exploits a simple but novel technique for breaking the synthesis problem into parts: each of our transformers is the meet of a collection of simpler, sound transformers that are synthesized such that each new piece fills a gap in the precision of the final transformer. Our design point is bulk automation: no sketches are required. Transformers are verified by lowering to a previously-created SMT dialect of MLIR. Each of our synthesized transformers is provably sound and some (17 %) are more precise than those provided by LLVM.\n                  <\/jats:p>","DOI":"10.1145\/3776722","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"2323-2351","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8613-3506","authenticated-orcid":false,"given":"Xuanyu","family":"Peng","sequence":"first","affiliation":[{"name":"University of California, San Diego, La Jolla, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7368-4333","authenticated-orcid":false,"given":"Dominic","family":"Kennedy","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-5742-0692","authenticated-orcid":false,"given":"Yuyou","family":"Fan","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7078-9287","authenticated-orcid":false,"given":"Ben","family":"Greenman","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7025-4610","authenticated-orcid":false,"given":"John","family":"Regehr","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9625-4037","authenticated-orcid":false,"given":"Loris","family":"D'Antoni","sequence":"additional","affiliation":[{"name":"University of California, San Diego, La Jolla, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_2","first-page":"14","article-title":"The SMT-LIB standard: Version 2.0","volume":"13","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett, Pascal Fontaine, and Cesare Tinelli. 2010. The SMT-LIB standard: Version 2.0. In Workshop on Satisfiability Modulo Theories, Vol. 13. 14. https:\/\/smt-lib.org\/papers\/smt-lib-reference-v2.7-r2025-02-05.pdf.","journal-title":"Workshop on Satisfiability Modulo Theories"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-44245-2_7"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45260-5_4"},{"key":"e_1_3_2_5_2","unstructured":"Compiler Research at The University of Cambridge. 2025. xdsl-smt. https:\/\/github.com\/opencompl\/xdsl-smt Accessed 2025-11-25."},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55844-6_142"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS. 337\u2013340. doi:10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/2651361"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3729309"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2651360"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1093\/biomet\/57.1.97"},{"key":"e_1_3_2_14_2","unstructured":"Hatsunespica and OpenCompl Contributors. 2025. xdsl-smt: Artifact Branch. https:\/\/github.com\/Hatsunespica\/xdsl-smt\/tree\/artifact. Accessed: 2025-10-23."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_18"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563334"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-74776-2_6"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3763088"},{"key":"e_1_3_2_19_2","unstructured":"Nick Lewycky. 2015. Miscompile of % in loop. https:\/\/bugs.llvm.org\/show_bug.cgi?id=23011 Accessed 2025-11-25."},{"key":"e_1_3_2_20_2","unstructured":"LLVM Contributors. 2025. LLJIT Class Reference. https:\/\/llvm.org\/doxygen\/classllvm_1_1orc_1_1LLJIT.html Accessed 2025-11-25."},{"key":"e_1_3_2_21_2","volume-title":"Workshop on Quantitative Analysis of Software","author":"Logozzo Francesco","year":"2009","unstructured":"Francesco Logozzo. 2009. Towards a Quantitative Estimation of Abstract Interpretations. In Workshop on Quantitative Analysis of Software. Microsoft. https:\/\/www.microsoft.com\/en-us\/research\/publication\/towards-a-quantitative-estimation-of-abstract-interpretations\/."},{"key":"e_1_3_2_22_2","unstructured":"OpenCompl Contributors. 2025. Pull Request #73: xdsl-smt. https:\/\/github.com\/opencompl\/xdsl-smt\/pull\/73. Accessed: 2025-10-23."},{"key":"e_1_3_2_23_2","unstructured":"OpenCompl Contributors. 2025. Pull Request #74: xdsl-smt. https:\/\/github.com\/opencompl\/xdsl-smt\/pull\/74. Accessed: 2025-10-23."},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622861"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3720470"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","unstructured":"Xuanyu Peng Dominic Kennedy Yuyou Fan Ben Greenman John Regehr and Loris D\u2019Antoni. 2025. Artifact for Nice to Meet You: Synthesizing Practical Abstract Transformers for MLIR. doi:10.5281\/zenodo.17371668 Version v2.","DOI":"10.5281\/zenodo.17371668"},{"key":"e_1_3_2_27_2","unstructured":"John Regehr. 2012. Wrong code bug. https:\/\/bugs.llvm.org\/show_bug.cgi?id=12541 Accessed 2025-11-25."},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/1024393.1024410"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","unstructured":"Thomas W. Reps Shmuel Sagiv and Greta Yorsh. 2004. Symbolic Implementation of the Best Transformer. In VMCAI. 252\u2013266. doi:10.1007\/978-3-540-24622-0_21","DOI":"10.1007\/978-3-540-24622-0_21"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_1"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250750"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451150"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"Aditya V. Thakur Matt Elder and Thomas W. Reps. 2012. Bilateral Algorithms for Symbolic Abstraction. In SAS. 111\u2013128. doi:10.1007\/978-3-642-33125-1_10","DOI":"10.1007\/978-3-642-33125-1_10"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.02.003"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","unstructured":"Aditya V. Thakur and Thomas W. Reps. 2012. A Method for Symbolic Computation of Abstract Operations. In CAV. 174\u2013192. doi:10.1007\/978-3-642-31424-7_17","DOI":"10.1007\/978-3-642-31424-7_17"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776722","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:41:36Z","timestamp":1784209296000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776722"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":35,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776722"],"URL":"https:\/\/doi.org\/10.1145\/3776722","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}