{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:48:46Z","timestamp":1775868526508,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":47,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,4,2]],"date-time":"2024-04-02T00:00:00Z","timestamp":1712016000000},"content-version":"vor","delay-in-days":1,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"U.S. National Science Foundation","award":["1750399, 2019306"],"award-info":[{"award-number":["1750399, 2019306"]}]},{"name":"Intel Strategic Research Alliance"},{"name":"DARPA","award":["ACE, center in Jump 2.0"],"award-info":[{"award-number":["ACE, center in Jump 2.0"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,4]]},"DOI":"10.1145\/3626202.3637563","type":"proceedings-article","created":{"date-parts":[[2024,4,2]],"date-time":"2024-04-02T18:04:51Z","timestamp":1712081091000},"page":"97-107","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Formal Verification of Source-to-Source Transformations for HLS"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5103-3097","authenticated-orcid":false,"given":"Louis-No\u00ebl","family":"Pouchet","sequence":"first","affiliation":[{"name":"Colorado State University, Fort Collins, CO, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-1447-5683","authenticated-orcid":false,"given":"Emily","family":"Tucker","sequence":"additional","affiliation":[{"name":"Colorado State University, Fort Collins, CO, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2850-0176","authenticated-orcid":false,"given":"Niansong","family":"Zhang","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6617-0075","authenticated-orcid":false,"given":"Hongzheng","family":"Chen","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3722-5126","authenticated-orcid":false,"given":"Debjit","family":"Pal","sequence":"additional","affiliation":[{"name":"University of Illinois at Chicago, Chicago, IL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0338-3655","authenticated-orcid":false,"given":"Gabriel","family":"Rodr\u00edguez","sequence":"additional","affiliation":[{"name":"CITIC, Universidade da Coru\u00f1a, A Coruna, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0778-0308","authenticated-orcid":false,"given":"Zhiru","family":"Zhang","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,4,2]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2022. ISA 0.13. http:\/\/repo.or.cz\/w\/isa.git"},{"key":"e_1_3_2_1_2_1","unstructured":"2023. The KLEE Symbolic Execution Engine. https:\/\/klee.github.io"},{"key":"e_1_3_2_1_3_1","unstructured":"2023. PoCC the Polyhedral Compiler Collection 1.6. https:\/\/pocc.sourceforge.net"},{"key":"e_1_3_2_1_4_1","unstructured":"2023. Programming in C. https:\/\/www.quut.com\/c\/"},{"key":"e_1_3_2_1_5_1","volume-title":"28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering.","author":"Badihi Sahar","year":"2020","unstructured":"Sahar Badihi, Faridah Akinotcho, Yi Li, and Julia Rubin. 2020. ARDi\u00ff: scaling pro- gram equivalence checking via iterative abstraction and re\u00ffnement of common code. In 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering."},{"key":"e_1_3_2_1_6_1","volume-title":"Proceedings of the 43rd Annual ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages.","author":"Bao Wenlei","unstructured":"Wenlei Bao, Sriram Krishnamoorthy, Louis-No\u00ebl Pouchet, Fabrice Rastello, and P. Sadayappan. 2016. PolyCheck: Dynamic Veri\u00ffcation of Iteration Space Transfor- mations on A\u00ffne Programs. In Proceedings of the 43rd Annual ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages."},{"key":"e_1_3_2_1_7_1","volume-title":"Veri\u00ffcation of Scheduling of Conditional Behaviors in High-Level Synthesis","author":"Chouksey Ramanuj","year":"2020","unstructured":"Ramanuj Chouksey and Chandan Karfa. 2020. Veri\u00ffcation of Scheduling of Conditional Behaviors in High-Level Synthesis. IEEE Transactions on Very Large Scale Integration (VLSI) Systems (2020)."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527328"},{"key":"e_1_3_2_1_9_1","volume-title":"FPGA HLS today: successes, challenges, and opportunities. ACM Transactions on Recon\u00ffgurable Technology and Systems (TRETS)","author":"Cong Jason","year":"2022","unstructured":"Jason Cong, Jason Lau, Gai Liu, Stephen Neuendor\u00ffer, Peichen Pan, Kees Vissers, and Zhiru Zhang. 2022. FPGA HLS today: successes, challenges, and opportunities. ACM Transactions on Recon\u00ffgurable Technology and Systems (TRETS) (2022)."},{"key":"e_1_3_2_1_10_1","volume-title":"High-level synthesis for FPGAs: From prototyping to de- ployment","author":"Cong Jason","year":"2011","unstructured":"Jason Cong, Bin Liu, Stephen Neuendor\u00ffer, Juanjo Noguera, Kees Vissers, and Zhiru Zhang. 2011. High-level synthesis for FPGAs: From prototyping to de- ployment. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (2011)."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3240765.3240838"},{"key":"e_1_3_2_1_12_1","volume-title":"Proceed- ings of the 4th international conference on NASA Formal Methods.","author":"Cousot Patrick","unstructured":"Patrick Cousot. 2012. Formal Veri\u00ffcation by Abstract Interpretation. In Proceed- ings of the 4th international conference on NASA Formal Methods."},{"key":"e_1_3_2_1_13_1","volume-title":"Bert: Pre-training of deep bidirectional transformers for language understanding. arXiv preprint arXiv:1810.04805","author":"Devlin Jacob","year":"2018","unstructured":"Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. 2018. Bert: Pre-training of deep bidirectional transformers for language understanding. arXiv preprint arXiv:1810.04805 (2018)."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677010"},{"key":"e_1_3_2_1_15_1","volume-title":"International Journal of Parallel Programming","author":"Feautrier P.","year":"1992","unstructured":"P. Feautrier. 1992. Some e\u00ffcient solutions to the a\u00ffne scheduling problem, part II: multidimensional time. International Journal of Parallel Programming (1992)."},{"key":"e_1_3_2_1_16_1","unstructured":"Cornell Zhang Group. 2023. HeteroCL: A Multi-Paradigm Programming Infras- tructure for Software-De\u00ffned Recon\u00ffgurable Computing. https:\/\/github.com\/ cornell-zhang\/heterocl\/releases\/tag\/v0.5"},{"key":"e_1_3_2_1_17_1","volume-title":"Proc. ACM Program. Lang.","author":"Herklotz Yann","year":"2021","unstructured":"Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson. 2021. Formal Veri\u00ffcation of High-Level Synthesis. Proc. ACM Program. Lang. (2021)."},{"key":"e_1_3_2_1_18_1","unstructured":"Intel. 2023. High Level Synthesis (HLS) Design Examples and Tutori- als. https:\/\/www.intel.com\/content\/www\/us\/en\/docs\/programmable\/683053\/19- 1\/high-level-synthesis-hls-design-examples.html"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3466752.3480092"},{"key":"e_1_3_2_1_20_1","volume-title":"Veri\u00ffcation of loop and arithmetic transformations of array-intensive behaviors","author":"Karfa Chandan","year":"2013","unstructured":"Chandan Karfa, Kunal Banerjee, Dipankar Sarkar, and Chittaranjan Mandal. 2013. Veri\u00ffcation of loop and arithmetic transformations of array-intensive behaviors. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems (2013)."},{"key":"e_1_3_2_1_21_1","volume-title":"7th International Symposium on Quality Electronic Design (ISQED'06)","author":"Karfa C.","unstructured":"C. Karfa, C. Mandal, D. Sarkar, S.R. Pentakota, and C. Reade. 2006. A formal veri\u00ffcation method of scheduling in high-level synthesis. In 7th International Symposium on Quality Electronic Design (ISQED'06)."},{"key":"e_1_3_2_1_22_1","unstructured":"Sehoon Kim Coleman Hooper Thanakul Wattanawong Minwoo Kang Ruohan Yan Hasan Genc Grace Dinh Qijing Huang Kurt Keutzer Michael W Mahoney et al. 2023. Full stack optimization of transformer inference: a survey. arXiv preprint arXiv:2302.14017 (2023)."},{"key":"e_1_3_2_1_23_1","volume-title":"Proceedings of the Great Lakes Symposium on VLSI.","author":"Klemmer Lucas","year":"2021","unstructured":"Lucas Klemmer and Daniel Gro\u00dfe. 2021. EPEX: processor veri\u00ffcation by equiva- lent program execution. In Proceedings of the Great Lakes Symposium on VLSI."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2023.3271065"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3289602.3293910"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3400302.3415644"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3469660"},{"key":"e_1_3_2_1_28_1","volume-title":"IEEE\/ACM International Symposium on Code Generation and Optimization.","author":"Lattner Chris","year":"2021","unstructured":"Chris Lattner, Mehdi Amini, Uday Bondhugula, Albert Cohen, Andy Davis, Jacques Pienaar, River Riddle, Tatiana Shpeisman, Nicolas Vasilache, and Olek- sandr Zinenko. 2021. MLIR: Scaling compiler infrastructure for domain speci\u00ffc computation. In IEEE\/ACM International Symposium on Code Generation and Optimization."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115670"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Nuno P Lopes Juneyoung Lee Chung-Kil Hur Zhengyang Liu and John Regehr. 2021. Alive2: bounded translation validation for LLVM. In ACM SIGPLAN Inter- national Conference on Programming Language Design and Implementation.","DOI":"10.1145\/3453483.3454030"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/MDT.2009.79"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385989"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3489517.3530681"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","unstructured":"Louis-Noel Pouchet and Emily Tucker. 2023. PAST the PoCC AST Library version 0.7.2. https:\/\/sourceforge.net\/projects\/pocc\/\u00ffles\/1.6\/testing\/modules\/past-0.7.2. tar.gz https:\/\/doi.org\/10.5281\/zenodo.10449349","DOI":"10.5281\/zenodo.10449349"},{"key":"e_1_3_2_1_37_1","unstructured":"Louis-Noel Pouchet and Tomofumi Yuki. 2023. PolyBench\/C 4.2.1. https: \/\/polybench.sourceforge.net"},{"key":"e_1_3_2_1_38_1","volume-title":"24th {USENIX} Security Symposium ({USENIX} Security 15).","author":"Ramos David A","unstructured":"David A Ramos and Dawson Engler. 2015. Under-constrained symbolic execu- tion: Correctness checking for real code. In 24th {USENIX} Security Symposium ({USENIX} Security 15)."},{"key":"e_1_3_2_1_39_1","volume-title":"Veri\u00ffcation of Source Code Transformations by Program Equivalence Checking. CC","author":"Shashidhar KC","year":"2005","unstructured":"KC Shashidhar, Maurice Bruynooghe, Francky Catthoor, and Gerda Janssens. 2005. Veri\u00ffcation of Source Code Transformations by Program Equivalence Checking. CC (2005)."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/FCCM.2019.00033"},{"key":"e_1_3_2_1_41_1","volume-title":"Attention is all you need. Advances in neural information processing systems 30","author":"Vaswani Ashish","year":"2017","unstructured":"Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Aukasz Kaiser, and Illia Polosukhin. 2017. Attention is all you need. Advances in neural information processing systems 30 (2017)."},{"key":"e_1_3_2_1_42_1","volume-title":"Equivalence checking of static a\u00ffne programs using widening to handle recurrences. ACM Trans. on Programming Languages and Systems (TOPLAS)","author":"Verdoolaege Sven","year":"2012","unstructured":"Sven Verdoolaege, Gerda Janssens, and Maurice Bruynooghe. 2012. Equivalence checking of static a\u00ffne programs using widening to handle recurrences. ACM Trans. on Programming Languages and Systems (TOPLAS) (2012)."},{"key":"e_1_3_2_1_43_1","volume-title":"The 2021 ACM\/SIGDA International Symposium on Field-Programmable Gate Arrays.","author":"Guo Licheng","year":"2021","unstructured":"JieWang, Licheng Guo, and Jason Cong. 2021. AutoSA: A polyhedral compiler for high-performance systolic arrays on FPGA. In The 2021 ACM\/SIGDA International Symposium on Field-Programmable Gate Arrays."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.14778\/3407790.3407799"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434304"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3490422.3502369"},{"key":"e_1_3_2_1_47_1","unstructured":"AMD Xilinx. 2022. Merlin. https:\/\/github.com\/Xilinx\/merlin-compiler"}],"event":{"name":"FPGA '24: The 2024 ACM\/SIGDA International Symposium on Field Programmable Gate Arrays","location":"Monterey CA USA","acronym":"FPGA '24","sponsor":["SIGDA ACM Special Interest Group on Design Automation"]},"container-title":["Proceedings of the 2024 ACM\/SIGDA International Symposium on Field Programmable Gate Arrays"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3626202.3637563","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3626202.3637563","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3626202.3637563","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T22:04:24Z","timestamp":1755900264000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3626202.3637563"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4]]},"references-count":47,"alternative-id":["10.1145\/3626202.3637563","10.1145\/3626202"],"URL":"https:\/\/doi.org\/10.1145\/3626202.3637563","relation":{},"subject":[],"published":{"date-parts":[[2024,4]]},"assertion":[{"value":"2024-04-02","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}