{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:45Z","timestamp":1780994625731,"version":"3.54.1"},"reference-count":64,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-22-CE39-0014-03"],"award-info":[{"award-number":["ANR-22-CE39-0014-03"]}],"id":[{"id":"10.13039\/501100001665","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":[[2024,6,20]]},"abstract":"<jats:p>Rewriting and static analyses are mutually beneficial techniques: program transformations change the inten- sional aspects of the program, and can thus improve analysis precision, while some efficient transformations are enabled by specific knowledge of some program invariants. Despite the strong interaction between these techniques, they are usually considered distinct. In this paper, we demonstrate that we can turn abstract interpreters into compilers, using a simple free algebra over the standard signature of abstract domains. Functor domains correspond to compiler passes, for which soundness is translated to a proof of forward simulation, and completeness to backward simulation. We achieve translation to SSA using an abstract domain with a non-standard SSA signature. Incorporating such an SSA translation to an abstract interpreter improves its precision; in particular we show that an SSA-based non-relational domain is always more precise than a standard non-relational domain for similar time and memory complexity. Moreover, such a domain allows recovering from precision losses that occur when analyzing low-level machine code instead of source code. These results help implement analyses or compilation passes where symbolic and semantic methods simultaneously refine each other, and improves precision when compared to doing the passes in sequence.<\/jats:p>\n          <jats:p>\n            CCS Concepts: \u2022\n            <jats:bold>Software and its engineering \u2192 Compilers<\/jats:bold>\n            ;\n            <jats:italic toggle=\"yes\">Formal Software verification;<\/jats:italic>\n            \u2022\n            <jats:bold>Theory of computation \u2192 Program analysis<\/jats:bold>\n            ;\n            <jats:bold>Program verification<\/jats:bold>\n            ;\n            <jats:bold>Abstraction<\/jats:bold>\n            ;\n            <jats:italic toggle=\"yes\">Equational logic and rewriting.<\/jats:italic>\n          <\/jats:p>","DOI":"10.1145\/3656392","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"368-393","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Compiling with Abstract Interpretation"],"prefix":"10.1145","volume":"8","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"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73561"},{"key":"e_1_3_1_3_1","article-title":"Program Logics - for Certified Compilers","author":"Appel Andrew W.","year":"2014","unstructured":"Andrew W. Appel. 2014. Program Logics - for Certified Compilers. Cambridge University Press.","journal-title":"Cambridge University Press"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.3233\/fi-1996-263401"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46423-9_8"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1749608.1749612"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/4304.003.0024"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290357"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","unstructured":"J\u00e9r\u00f4me Boillot and Jerome Feret. 2023. Symbolic Transformation of Expressions in Modular Arithmetic. (10 2023) 84-113. https:\/\/doi.org\/10.1007\/978-3-031-44245-2_6 10.1007\/978-3-031-44245-2_6","DOI":"10.1007\/978-3-031-44245-2_6"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/bfb0039704"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197331"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37051-9_6"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371096"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007205"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_11"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/201059.201061"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/202529.202534"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","unstructured":"Patrick Cousot and Radhia Cousot. 2002. Systematic design of program transformation frameworks by abstract interpretation. In 29th Symposium on Principles of Programming Languages (POPL 2002) John Launchbury and John C. Mitchell (Eds.). ACM 178-190. https:\/\/doi.org\/10.1145\/503272.503290 10.1145\/503272.503290","DOI":"10.1145\/503272.503290"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77505-8_23"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110256"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814308"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3178372.3179503"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_15"},{"key":"e_1_3_1_27_1","article-title":"Operational refinement for compiler correctness","author":"Dockins Robert W","year":"2012","unstructured":"Robert W Dockins. 2012. Operational refinement for compiler correctness. Ph.D. Dissertation. Princeton University.","journal-title":"Ph.D. Dissertation. Princeton University"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159876.1159880"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_4"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676987"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56287-7_95"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27864-1_17"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_2"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676966"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-41600-3_1"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360602"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/202529.202532"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/512927.512945"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32202-0_3"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571258"},{"key":"e_1_3_1_41_1","article-title":"The Codex semantic library","author":"Lemerre Matthieu","year":"2024","unstructured":"Matthieu Lemerre, Julien Simonnet, Olivier Nicole, Dorian Lesbre, Iker Canut, Corentin Gendreau, and Guillaume Girol. 2024. The Codex semantic library. https:\/\/github.com\/codex-semantics-library\/codex. Version 1.0-beta.","journal-title":"https:\/\/github.com\/codex-semantics-library\/codex. Version 1.0-beta"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503298"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","unstructured":"Dorian Lesbre and Matthieu Lemerre. 2024a. Compiling with Abstract Interpetation: Artifact. https:\/\/doi.org\/10.5281\/zenodo.10895582 10.5281\/zenodo.10895582","DOI":"10.5281\/zenodo.10895582"},{"key":"e_1_3_1_45_1","article-title":"Compiling with Abstract Interpretation (with appendices)","author":"Lesbre Dorian","year":"2024","unstructured":"Dorian Lesbre and Matthieu Lemerre. 2024b. Compiling with Abstract Interpretation (with appendices). Technical Report. https:\/\/hal.science\/hal-04535159","journal-title":"Technical Report"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78791-4_14"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33558-7_39"},{"key":"e_1_3_1_48_1","article-title":"Weakly relational numerical abstract domains","author":"Mine A.","year":"2004","unstructured":"A. Mine. 2004. Weakly relational numerical abstract domains. Ph.D. Dissertation. Ecole Polytechnique. http:\/\/www.di.ens.fr\/~mine\/these\/these-color.pdf.","journal-title":"Ph.D. Dissertation. Ecole Polytechnique"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_23"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.29007\/b63g"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000034"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS52030.2021.00011"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-94583-1_11"},{"key":"e_1_3_1_54_1","article-title":"SSA-based Compiler Design","author":"Rastello Fabrice","year":"2022","unstructured":"Fabrice Rastello and Florent Bouchez Tichadou (Eds.). 2022. SSA-based Compiler Design. Springer.","journal-title":"Springer"},{"key":"e_1_3_1_55_1","article-title":"Lightweight modular staging and embedded compilers: Abstraction without regret for high-level highperformanceprogramming","author":"Rompf Tiark","year":"2012","unstructured":"Tiark Rompf. 2012. Lightweight modular staging and embedded compilers: Abstraction without regret for high-level highperformanceprogramming. Ph.D. Dissertation. Ecole Polytechnique Federale de Lausanne.","journal-title":"Ph.D. Dissertation. Ecole Polytechnique Federale de Lausanne"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73562"},{"key":"e_1_3_1_57_1","first-page":"397","article-title":"An overview of the K semantic framework. J. Log","author":"Ro\u015fu Grigore","year":"2010","unstructured":"Grigore Ro\u015fu and Traian-Florin Serbanuta. 2010. An overview of the K semantic framework. J. Log. Algebraic Methods Program. 79 (2010), 397-434. https:\/\/api.semanticscholar.org\/CorpusID:13756844","journal-title":"Algebraic Methods Program. 79 (2010)"},{"key":"e_1_3_1_58_1","article-title":"Semantics of an intermediate language for program transformation","author":"Schneider Sigurd","year":"2013","unstructured":"Sigurd Schneider. 2013. Semantics of an intermediate language for program transformation. preparation. Master\u2019s Thesis. Universit\u00e4t des Saarlandes (2013).","journal-title":"preparation. Master\u2019s Thesis. Universit\u00e4t des Saarlandes (2013)"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491979"},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199464"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61739-6_53"},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO53902.2022.9741267"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/103135.103136"},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010248"},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656392","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656392","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:39:43Z","timestamp":1751661583000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656392"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":64,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656392"],"URL":"https:\/\/doi.org\/10.1145\/3656392","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}