{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T11:01:29Z","timestamp":1790679689763,"version":"4.1.0"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T00:00:00Z","timestamp":1651190400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,4,29]]},"abstract":"<jats:p>\n            This paper considers the correctness of domain-specific compilers for tensor programming languages through the study of Halide, a popular representative. It describes a translation validation algorithm for\n            <jats:italic>affine<\/jats:italic>\n            Halide specifications, independently of the scheduling language. The algorithm relies on \u201cprophetic\u201d annotations added by the compiler to the generated array assignments. The annotations provide a refinement mapping from assignments in the generated code to the tensor definitions from the specification. Our implementation leverages an affine solver and a general SMT solver, and scales to complete Halide benchmarks.\n          <\/jats:p>","DOI":"10.1145\/3527328","type":"journal-article","created":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T15:42:03Z","timestamp":1651246923000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["End-to-end translation validation for the halide language"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9126-0937","authenticated-orcid":false,"given":"Basile","family":"Cl\u00e9ment","sequence":"first","affiliation":[{"name":"Inria, France \/ ENS Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8866-5343","authenticated-orcid":false,"given":"Albert","family":"Cohen","sequence":"additional","affiliation":[{"name":"Google, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,4,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5115"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854038.2854048"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980930.2907954"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837656"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 8th International Workshop on Satisfiability modulo Theories","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 ( Edinburgh, UK), A. Gupta and D. Kroening (Eds.). 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 (Edinburgh, UK), A. Gupta and D. Kroening (Eds.)."},{"key":"e_1_2_1_6_1","volume-title":"17th International Conference, CAV 2005 (Lncs","volume":"295","author":"Barrett Clark W.","unstructured":"Clark W. Barrett , Yi Fang , Benjamin Goldberg , Ying Hu , Amir Pnueli , and Lenore D. Zuck . 2005. TVOC: A Translation Validator for Optimizing Compilers. In Computer Aided Verification , 17th International Conference, CAV 2005 (Lncs , Vol. 3576). springer, 291\u2013 295 . Clark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, and Lenore D. Zuck. 2005. TVOC: A Translation Validator for Optimizing Compilers. In Computer Aided Verification, 17th International Conference, CAV 2005 (Lncs, Vol. 3576). springer, 291\u2013295."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45706-2_40"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/jproc.2004.840311"},{"key":"e_1_2_1_9_1","unstructured":"Fran\u00e7ois Bobot Jean-Christophe Filli\u00e2tre Claude March\u00e9 and Andrei Paskevich. 2011. Why3: Shepherd Your Herd of Provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages. Wroc\u0142 aw Poland. 53\u201364.  Fran\u00e7ois Bobot Jean-Christophe Filli\u00e2tre Claude March\u00e9 and Andrei Paskevich. 2011. Why3: Shepherd Your Herd of Provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages. Wroc\u0142 aw Poland. 53\u201364."},{"key":"e_1_2_1_10_1","volume-title":"Automatic Transformations for Communication-Minimized Parallelization and Locality Optimization in the Polyhedral Model. In International Conference on Compiler Construction (ETAPS CC).","author":"Bondhugula Uday","unstructured":"Uday Bondhugula , Muthu Baskaran , Sriram Krishnamoorthy , J. Ramanujam , A. Rountev , and P. Sadayappan . 2008 . Automatic Transformations for Communication-Minimized Parallelization and Locality Optimization in the Polyhedral Model. In International Conference on Compiler Construction (ETAPS CC). Uday Bondhugula, Muthu Baskaran, Sriram Krishnamoorthy, J. Ramanujam, A. Rountev, and P. Sadayappan. 2008. Automatic Transformations for Communication-Minimized Parallelization and Locality Optimization in the Polyhedral Model. In International Conference on Compiler Construction (ETAPS CC)."},{"key":"e_1_2_1_11_1","volume-title":"ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI).","author":"Bondhugula Uday","unstructured":"Uday Bondhugula , Albert Hartono , J. Ramanujam , and P. Sadayappan . 2008. A Practical Automatic Polyhedral Program Optimization System . In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). Uday Bondhugula, Albert Hartono, J. Ramanujam, and P. Sadayappan. 2008. A Practical Automatic Polyhedral Program Optimization System. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6390003"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434321"},{"key":"e_1_2_1_14_1","volume-title":"Dealing with Arithmetic Overflows in the Polyhedral Model. In IMPACT 2012 - 2nd International Workshop on Polyhedral Compilation Techniques, Uday Bondhugula and Vincent Loechner (Eds.)","author":"Parrino Bruno Cuervo","year":"2012","unstructured":"Bruno Cuervo Parrino , Julien Narboux , Eric Violard , and Nicolas Magaud . 2012 . Dealing with Arithmetic Overflows in the Polyhedral Model. In IMPACT 2012 - 2nd International Workshop on Polyhedral Compilation Techniques, Uday Bondhugula and Vincent Loechner (Eds.) . Paris, France. https:\/\/hal.inria.fr\/hal-00655485 Bruno Cuervo Parrino, Julien Narboux, Eric Violard, and Nicolas Magaud. 2012. Dealing with Arithmetic Overflows in the Polyhedral Model. In IMPACT 2012 - 2nd International Workshop on Polyhedral Compilation Techniques, Uday Bondhugula and Vincent Loechner (Eds.). Paris, France. https:\/\/hal.inria.fr\/hal-00655485"},{"key":"e_1_2_1_15_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"de Moura Leonardo","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner . 2008. Z3: An Efficient SMT Solver . In Tools and Algorithms for the Construction and Analysis of Systems , C.R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 337\u2013340. isbn:978-3-540-78800-3 Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, C.R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 337\u2013340. isbn:978-3-540-78800-3"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2017.7863748"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1051\/ro\/1988220302431"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/bf01407931"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2743016"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10936-7_11"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0311-x"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2528228.2528231"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/tcad.2013.2272536"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/321406.321418"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1543135.1542513"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00925828"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53413-7_16"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/mm.2019.2928962"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2897824.2925952"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775054.2694364"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_2_1_33_1","volume-title":"Tools and Algorithms for Construction and Analysis of Systems, TACAS \u201998 (Lncs","author":"Pnueli Amir","unstructured":"Amir Pnueli , Michael Siegel , and Eli Singerman . 1998. Translation Validation . In Tools and Algorithms for Construction and Analysis of Systems, TACAS \u201998 (Lncs , Vol. 1384). springer, 151\u2013 166 . Amir Pnueli, Michael Siegel, and Eli Singerman. 1998. Translation Validation. In Tools and Algorithms for Construction and Analysis of Systems, TACAS \u201998 (Lncs, Vol. 1384). springer, 151\u2013166."},{"key":"e_1_2_1_34_1","volume-title":"Welchem Die Addition Als Einzige Operation Hervortritt. In Comptes Rendus Du Premier Congr\u00e8s de Math\u00e9maticiens Des Pays Slaves.","author":"Presburger M.","unstructured":"M. Presburger . 1929. \u00dcber Die Vollst\u00e4ndigkeit Eines Gewissen Systems Der Arithmetik Ganzer Zahlen , in Welchem Die Addition Als Einzige Operation Hervortritt. In Comptes Rendus Du Premier Congr\u00e8s de Math\u00e9maticiens Des Pays Slaves. Warsaw, Poland . 92\u2013101. M. Presburger. 1929. \u00dcber Die Vollst\u00e4ndigkeit Eines Gewissen Systems Der Arithmetik Ganzer Zahlen, in Welchem Die Addition Als Einzige Operation Hervortritt. In Comptes Rendus Du Premier Congr\u00e8s de Math\u00e9maticiens Des Pays Slaves. Warsaw, Poland. 92\u2013101."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2185520.2185528"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3150211"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462176"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3315454.3329959"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/224486.224533"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31985-6_15"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/3049832.3049863"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.2168\/lmcs-7(1:10)2011"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4501022"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993316.1993533"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1707801.1706311"},{"key":"e_1_2_1_46_1","volume-title":"Tensor Comprehensions: Framework-agnostic High-Performance Machine Learning Abstractions. arxiv:1802.04730.","author":"Vasilache Nicolas","year":"2018","unstructured":"Nicolas Vasilache , Oleksandr Zinenko , Theodoros Theodoridis , Priya Goyal , Zachary DeVito , William S. Moses , Sven Verdoolaege , Andrew Adams , and Albert Cohen . 2018 . Tensor Comprehensions: Framework-agnostic High-Performance Machine Learning Abstractions. arxiv:1802.04730. Nicolas Vasilache, Oleksandr Zinenko, Theodoros Theodoridis, Priya Goyal, Zachary DeVito, William S. Moses, Sven Verdoolaege, Andrew Adams, and Albert Cohen. 2018. Tensor Comprehensions: Framework-agnostic High-Performance Machine Learning Abstractions. arxiv:1802.04730."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3355606"},{"key":"e_1_2_1_48_1","volume-title":"Isl: An Integer Set Library for the Polyhedral Model.","author":"Verdoolaege Sven","year":"2010","unstructured":"Sven Verdoolaege . 2010 . Isl: An Integer Set Library for the Polyhedral Model. . In ICMS, Komei Fukuda, Joris van der Hoeven, Michael Joswig, and Nobuki Takayama (Eds.) (Lecture Notes in Computer Science, Vol . 6327). Springer , 299\u2013302. isbn:978-3-642-15581-9 http:\/\/dblp.uni-trier.de\/db\/conf\/icms\/icms2010.html##Verdoolaege10 Sven Verdoolaege. 2010. Isl: An Integer Set Library for the Polyhedral Model.. In ICMS, Komei Fukuda, Joris van der Hoeven, Michael Joswig, and Nobuki Takayama (Eds.) (Lecture Notes in Computer Science, Vol. 6327). Springer, 299\u2013302. isbn:978-3-642-15581-9 http:\/\/dblp.uni-trier.de\/db\/conf\/icms\/icms2010.html##Verdoolaege10"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362390"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10836-009-5140-4"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3177961"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527328","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3527328","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:53Z","timestamp":1750191533000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527328"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,29]]},"references-count":51,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2022,4,29]]}},"alternative-id":["10.1145\/3527328"],"URL":"https:\/\/doi.org\/10.1145\/3527328","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,29]]},"assertion":[{"value":"2022-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}