{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T00:34:46Z","timestamp":1767918886416,"version":"3.49.0"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","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>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 abstract transformers 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).  \nWe developed NiceToMeetYou: 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.<\/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":[{"role":"author","vocabulary":"crossref"}]},{"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":[{"role":"author","vocabulary":"crossref"}]},{"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":[{"role":"author","vocabulary":"crossref"}]},{"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":[{"role":"author","vocabulary":"crossref"}]},{"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":[{"role":"author","vocabulary":"crossref"}]},{"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":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Workshop on Satisfiability Modulo Theories. 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. 13, 14. https:\/\/smt-lib.org\/papers\/smt-lib-reference-v2.7-r2025-02-05.pdf"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-44245-2_7"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45260-5_4"},{"key":"e_1_2_1_4_1","unstructured":"Compiler Research at The University of Cambridge. 2025. xdsl-smt. https:\/\/github.com\/opencompl\/xdsl-smt"},{"key":"e_1_2_1_5_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. ACM 238\u2013252. https:\/\/doi.org\/10.1145\/512950.512973 10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","unstructured":"Patrick Cousot and Radhia Cousot. 1979. Systematic Design of Program Analysis Frameworks. In POPL. ACM 269\u2013282. https:\/\/doi.org\/10.1145\/567752.567778 10.1145\/567752.567778","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55844-6_142"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS. 337\u2013340. isbn:3540787992 https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24 10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2651361"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3729309"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2651360"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1093\/biomet\/57.1.97"},{"key":"e_1_2_1_13_1","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_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_18"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563334"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-74776-2_6"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3763088"},{"key":"e_1_2_1_18_1","unstructured":"Nick Lewycky. 2015. Miscompile of % in loop. https:\/\/bugs.llvm.org\/show_bug.cgi?id=23011"},{"key":"e_1_2_1_19_1","unstructured":"LLVM Contributors. 2025. LLJIT Class Reference. https:\/\/llvm.org\/doxygen\/classllvm_1_1orc_1_1LLJIT.html"},{"key":"e_1_2_1_20_1","volume-title":"Workshop on Quantitative Analysis of Software. Microsoft. https:\/\/www.microsoft.com\/en-us\/research\/publication\/towards-a-quantitative-estimation-of-abstract-interpretations\/","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_2_1_21_1","unstructured":"OpenCompl Contributors. 2025. Pull Request #73: xdsl-smt. https:\/\/github.com\/opencompl\/xdsl-smt\/pull\/73 Accessed: 2025-10-23"},{"key":"e_1_2_1_22_1","unstructured":"OpenCompl Contributors. 2025. Pull Request #74: xdsl-smt. https:\/\/github.com\/opencompl\/xdsl-smt\/pull\/74 Accessed: 2025-10-23"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622861"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3720470"},{"key":"e_1_2_1_25_1","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. https:\/\/doi.org\/10.5281\/zenodo.17371668 Version v2 10.5281\/zenodo.17371668","DOI":"10.5281\/zenodo.17371668"},{"key":"e_1_2_1_26_1","unstructured":"John Regehr. 2012. Wrong code bug. https:\/\/bugs.llvm.org\/show_bug.cgi?id=12541"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1024393.1024410"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","unstructured":"Thomas W. Reps Shmuel Sagiv and Greta Yorsh. 2004. Symbolic Implementation of the Best Transformer. In VMCAI. 252\u2013266. https:\/\/doi.org\/10.1007\/978-3-540-24622-0_21 10.1007\/978-3-540-24622-0_21","DOI":"10.1007\/978-3-540-24622-0_21"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_1"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","unstructured":"Erika Rice Scherpelz Sorin Lerner and Craig Chambers. 2007. Automatic Inference of Optimizer Flow Functions from Semantic Meanings. In PLDI. ACM 135\u2013145. https:\/\/doi.org\/10.1145\/1250734.1250750 10.1145\/1250734.1250750","DOI":"10.1145\/1250734.1250750"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","unstructured":"Eric Schkufza Rahul Sharma and Alex Aiken. 2013. Stochastic Superoptimization. In ASPLOS. ACM 305\u2013316. https:\/\/doi.org\/10.1145\/2451116.2451150 10.1145\/2451116.2451150","DOI":"10.1145\/2451116.2451150"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_10"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.02.003"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","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,1,8]],"date-time":"2026-01-08T19:02:12Z","timestamp":1767898932000},"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"}}]}}