{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T01:37:47Z","timestamp":1740101867063,"version":"3.37.3"},"reference-count":20,"publisher":"IEEE","license":[{"start":{"date-parts":[[2023,4,1]],"date-time":"2023-04-01T00:00:00Z","timestamp":1680307200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,4,1]],"date-time":"2023-04-01T00:00:00Z","timestamp":1680307200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/100000028","name":"Semiconductor Research Corporation","doi-asserted-by":"publisher","award":["2932.001"],"award-info":[{"award-number":["2932.001"]}],"id":[{"id":"10.13039\/100000028","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100002418","name":"Intel Corporation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100002418","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,4]]},"DOI":"10.23919\/date56975.2023.10137308","type":"proceedings-article","created":{"date-parts":[[2023,6,2]],"date-time":"2023-06-02T19:32:57Z","timestamp":1685734377000},"page":"1-6","source":"Crossref","is-referenced-by-count":0,"title":["An Automated Verification Framework for HalideIR-Based Compiler Transformations"],"prefix":"10.23919","author":[{"given":"Yanzhao","family":"Wang","sequence":"first","affiliation":[{"name":"Portland State University,Department of Computer Science,Portland,OR,USA,97201"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fei","family":"Xie","sequence":"additional","affiliation":[{"name":"Portland State University,Department of Computer Science,Portland,OR,USA,97201"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenkun","family":"Yang","sequence":"additional","affiliation":[{"name":"Intel Corporation,Strategic CAD Labs,Hillsboro,OR,USA,97124"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeremy","family":"Casas","sequence":"additional","affiliation":[{"name":"Intel Corporation,Strategic CAD Labs,Hillsboro,OR,USA,97124"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pasquale","family":"Cocchini","sequence":"additional","affiliation":[{"name":"Intel Corporation,Strategic CAD Labs,Hillsboro,OR,USA,97124"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jin","family":"Yang","sequence":"additional","affiliation":[{"name":"Intel Corporation,Strategic CAD Labs,Hillsboro,OR,USA,97124"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"ref12","first-page":"337","article-title":"Z3: An efficient smt solver","author":"de moura","year":"2008","journal-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054170"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/3428234"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/1543135.1542512"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454030"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/3373087.3375320"},{"journal-title":"Halide-to-hardware","year":"0","key":"ref2"},{"year":"0","key":"ref1"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462176"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/3107953"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328444"},{"journal-title":"Formal semantics for the halide language","year":"2020","author":"reinking","key":"ref18"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/3289602.3293910"},{"key":"ref9","article-title":"Compcert-a formally verified optimizing compiler","author":"leroy","year":"0","journal-title":"ERTS 2016 Embedded Real Time Software and Systems 8th European Congress"},{"key":"ref4","first-page":"209","article-title":"Klee: unassisted and automatic generation of high-coverage tests for complex systems programs","volume":"8","author":"cadar","year":"0","journal-title":"OSDI"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/2628071.2628092"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"ref5","first-page":"578","article-title":"{TVM}: An automated {End-to-End} optimizing compiler for deep learning","author":"chen","year":"0","journal-title":"13th USENIX Symposium on Operating Systems Design and Implementation (OSDI 18)"}],"event":{"name":"2023 Design, Automation & Test in Europe Conference & Exhibition (DATE)","start":{"date-parts":[[2023,4,17]]},"location":"Antwerp, Belgium","end":{"date-parts":[[2023,4,19]]}},"container-title":["2023 Design, Automation & Test in Europe Conference & Exhibition (DATE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/10136870\/10136706\/10137308.pdf?arnumber=10137308","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,26]],"date-time":"2023-06-26T17:53:21Z","timestamp":1687802001000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10137308\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4]]},"references-count":20,"URL":"https:\/\/doi.org\/10.23919\/date56975.2023.10137308","relation":{},"subject":[],"published":{"date-parts":[[2023,4]]}}}