{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T15:53:30Z","timestamp":1780674810362,"version":"3.54.1"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T00:00:00Z","timestamp":1749772800000},"content-version":"vor","delay-in-days":3,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/W007940\/1"],"award-info":[{"award-number":["EP\/W007940\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100018707","name":"HORIZON EUROPE Reforming and enhancing the European Research and Innovation system","doi-asserted-by":"publisher","award":["101070375"],"award-info":[{"award-number":["101070375"]}],"id":[{"id":"10.13039\/100018707","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1955688"],"award-info":[{"award-number":["1955688"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"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            MLIR is a toolkit supporting the development of extensible and composable intermediate representations (IRs) called\n            <jats:italic toggle=\"yes\">dialects<\/jats:italic>\n            ; it was created in response to rapid changes in hardware platforms, programming languages, and application domains such as machine learning. MLIR supports development teams creating compilers and compiler-adjacent tools by factoring out common infrastructure such as parsers and printers. A major limitation of MLIR is that it is syntax-focused: it has no support for directly encoding the semantics of operations in its dialects. Thus, at present, the parts of MLIR tools that depend on semantics\u2014optimizers, analyzers, verifiers, transformers\u2014must all be engineered by hand.\n          <\/jats:p>\n          <jats:p>Our work makes formal semantics a first-class citizen in the MLIR ecosystem. We designed and implemented a collection of semantics-supporting MLIR dialects for encoding the semantics of compiler IRs. These dialects support a separation of concerns between three domains of expertise when building formal-methods-based tooling for compilers. First, compiler developers define their dialect\u2019s semantics as a lowering (compilation transformation) from their dialect to one or more of ours. Second, SMT solver experts provide tools to optimize domain-specific high-level semantics and lower them to SMT queries. Third, tool builders create dialect-independent verification tools.<\/jats:p>\n          <jats:p>We validate our work by defining semantics for five key MLIR dialects, defining a state-of-the-art SMT encoding for memory-based semantics, and building three dialect-agnostic tools, which we used to find five miscompilation bugs in upstream MLIR, verify a canonicalization pass, and also formally verify transfer functions for two dataflow analyses: \u201cknown bits\u201d (that finds individual bits that are always zero or one in all executions) and \u201cdemanded bits\u201d (that finds don\u2019t-care bits). The transfer functions that we verify are improved versions of those in upstream MLIR; they detect on average 36.6% more known bits in real-world MLIR programs compared to the upstream implementation.<\/jats:p>","DOI":"10.1145\/3729309","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"1466-1490","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["First-Class Verification Dialects for MLIR"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4100-3190","authenticated-orcid":false,"given":"Mathieu","family":"Fehr","sequence":"first","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"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-8711-9976","authenticated-orcid":false,"given":"Hugo","family":"Pompougnac","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Grenoble Alpes, Grenoble, France"},{"name":"Inria Centre de Recherche Grenoble Rhone-Alpes, Grenoble, France"},{"name":"CNRS, Paris, France"},{"name":"Grenoble INP, Grenoble, France"}],"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-0003-3874-6003","authenticated-orcid":false,"given":"Tobias","family":"Grosser","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"The Rocket chip generator. EECS Department","author":"Asanovic Krste","year":"2016","unstructured":"Krste Asanovic, Rimas Avizienis, Jonathan Bachrach, Scott Beamer, David Biancolin, Christopher Celio, Henry Cook, Daniel Dabbelt, John Hauser, and Adam Izraelevitz. 2016. The Rocket chip generator. EECS Department, University of California, Berkeley, Tech. Rep. UCB\/EECS-2016-17, 4 (2016), 6\u20132."},{"key":"e_1_2_2_2_1","volume-title":"Synthesizable, Parameterized RISC-V Processor","author":"Asanovic Krste","unstructured":"Krste Asanovic, David A Patterson, and Christopher Celio. 2015. The Berkeley Out-of-Order Machine (BOOM): An Industry-Competitive, Synthesizable, Parameterized RISC-V Processor. University of California at Berkeley Berkeley United States, Tech. Rep."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2228360.2228584"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_19"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_2_2_6_1","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2024. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org"},{"key":"e_1_2_2_7_1","volume-title":"Proceedings of the 8th International Workshop on Satisfiability Modulo Theories. 13","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett, Aaron Stump, and Cesare Tinelli. 2010. The SMT-LIB standard: Version 2.0. In Proceedings of the 8th International Workshop on Satisfiability Modulo Theories. 13, 14."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2024.9"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385968"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO57630.2024.10444854"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","unstructured":"Mathieu Fehr. 2025. First-Class Verification Dialects for MLIR - PLDI 2025 Artifact. https:\/\/doi.org\/10.5281\/zenodo.15231119 10.5281\/zenodo.15231119","DOI":"10.5281\/zenodo.15231119"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3696443.3708945"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676966"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563334"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/977395.977673"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO51591.2021.9370308"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_35"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062343"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781156"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040335"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_2_25_1","volume-title":"CompCert - A Formally Verified Optimizing Compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress","author":"Leroy Xavier","year":"2016","unstructured":"Xavier Leroy, Sandrine Blazy, Daniel K\u00e4stner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. 2016. CompCert - A Formally Verified Optimizing Compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress. Toulouse, France. https:\/\/inria.hal.science\/hal-01238879"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454030"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737965"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692956.2663188"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616357"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649837"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428234"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29436-6_22"},{"key":"e_1_2_2_34_1","unstructured":"The Swift Project. 2024. Swift Intermediate Language (SIL). https:\/\/github.com\/swiftlang\/swift\/blob\/main\/docs\/SIL.rst"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1711.04422"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_59"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993533"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3617232.3624862"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103709"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462164"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729309","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729309","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T06:04:16Z","timestamp":1752645856000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729309"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":41,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729309"],"URL":"https:\/\/doi.org\/10.1145\/3729309","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-14","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"}}]}}