{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:58:18Z","timestamp":1790927898260,"version":"4.1.0"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T00:00:00Z","timestamp":1516665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2018,1,23]]},"abstract":"<jats:p>Compilers should not miscompile. Peephole optimizations, which perform local rewriting of the input program to improve the efficiency of generated code, are a persistent source of compiler bugs. We created Alive, a domain-specific language for writing optimizations and for automatically either proving them correct or else generating counterexamples. Furthermore, Alive can be automatically translated into C++ code that is suitable for inclusion in an LLVM optimization pass. Alive is based on an attempt to balance usability and formal methods; for example, it captures---but largely hides---the detailed semantics of the various kinds of undefined behavior. Alive has found numerous bugs in the LLVM compiler and is being used by LLVM developers.<\/jats:p>","DOI":"10.1145\/3166064","type":"journal-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T14:15:31Z","timestamp":1516716931000},"page":"84-91","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["Practical verification of peephole optimizations with Alive"],"prefix":"10.1145","volume":"61","author":[{"given":"Nuno P.","family":"Lopes","sequence":"first","affiliation":[{"name":"Microsoft Research, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Menendez","sequence":"additional","affiliation":[{"name":"Rutgers University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Santosh","family":"Nagarakatte","sequence":"additional","affiliation":[{"name":"Rutgers University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John","family":"Regehr","sequence":"additional","affiliation":[{"name":"University of Utah"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,1,23]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168906"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46663-6_9"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/502874.502885"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1186632.1186633"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542513"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594334"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062343"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737965"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0366-1"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/36206.36194"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062372"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53413-7_16"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491967"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2931021.2931024"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/646482.691453"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359569"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451150"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103709"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3166064","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3166064","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:26:55Z","timestamp":1750213615000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3166064"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,23]]},"references-count":21,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,1,23]]}},"alternative-id":["10.1145\/3166064"],"URL":"https:\/\/doi.org\/10.1145\/3166064","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,1,23]]},"assertion":[{"value":"2018-01-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}