{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T14:15:03Z","timestamp":1790691303911,"version":"4.1.0"},"reference-count":62,"publisher":"IEEE","license":[{"start":{"date-parts":[[2019,2,1]],"date-time":"2019-02-01T00:00:00Z","timestamp":1548979200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2019,2,1]],"date-time":"2019-02-01T00:00:00Z","timestamp":1548979200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2019,2,1]],"date-time":"2019-02-01T00:00:00Z","timestamp":1548979200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,2]]},"DOI":"10.1109\/cgo.2019.8661180","type":"proceedings-article","created":{"date-parts":[[2019,3,8]],"date-time":"2019-03-08T00:01:46Z","timestamp":1552003306000},"page":"37-49","source":"Crossref","is-referenced-by-count":11,"title":["Automatic Equivalence Checking for Assembly Implementations of Cryptography Libraries"],"prefix":"10.1109","author":[{"given":"Jay P.","family":"Lim","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Santosh","family":"Nagarakatte","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref39","author":"bernstein","year":"2007","journal-title":"qhasm tools to help write high-speed software"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/11745853_14"},{"key":"ref33","year":"2001"},{"key":"ref32","author":"bernstein","year":"2008","journal-title":"Chacha a variant of salsa20"},{"key":"ref31","year":"2015","journal-title":"FIPS PUB 180 Secure Hash Standard (SHS)"},{"key":"ref30","author":"ackermann","year":"1954","journal-title":"Solvable Cases of the Decision Problem"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660370"},{"key":"ref36","year":"2015","journal-title":"The Coq Proof Assistant Reference Manual"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3133974"},{"key":"ref60","first-page":"53","article-title":"Verifying constant-time implementations","author":"almeida","year":"2016","journal-title":"Proceedings of the 25th USENIX Conference on Security Symposium ser SEC’16"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660283"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53413-7_16"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737965"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"ref2","year":"2017"},{"key":"ref1","year":"2016"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-71237-6"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106281"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_31"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/3139337.3139343"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94144-8_22"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542513"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_5"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462164"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70389-3_2"},{"key":"ref59","author":"langley","year":"2010","journal-title":"Checking that functions are constant time with valgrind"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1145\/2892208.2892230"},{"key":"ref57","first-page":"263","article-title":"Equivalence checking using cuts and heaps","author":"kuehlmann","year":"1997","journal-title":"Proceedings of the 34th Annual Design Automation Conference ser DAC ’97"},{"key":"ref56","first-page":"229","article-title":"Sat sweeping with local observability don’t-cares","author":"zhu","year":"2006","journal-title":"Proceedings of the 43rd Annual Design Automation Conference Ser DAC '06"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1993.580110"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1145\/1086228.1086284"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1145\/3168821"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062372"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"},{"key":"ref11","article-title":"Vale: Verifying high-performance cryptographic assembly code","author":"bond","year":"2017","journal-title":"Proceedings of the 26th USENIX Conference on Security Symposium ser USENIX ’17"},{"key":"ref40","first-page":"174","article-title":"Boolector: An efficient smt solver for bitvectors and arrays","author":"brummayer","year":"2009","journal-title":"Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems Held As Part of the Joint European Conferences on Theory and Practice of Software ETAPS 2009 ser TACAS ’09"},{"key":"ref12","doi-asserted-by":"crossref","DOI":"10.1109\/SP.2019.00005","article-title":"Simple high-level code for cryptographic arithmetic - with proofs, without compromises","author":"erbsen","year":"2019","journal-title":"IEEE Symposium on Security & Privacy 2019 ser S&P’19"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48869-1_5"},{"key":"ref14","article-title":"Axe: An automated formal equivalence checking tool for programs","author":"smith","year":"2011","journal-title":"The Department of Computer Science"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509509"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382542"},{"key":"ref18","author":"lim","year":"2018","journal-title":"Casm-verify"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359569"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134078"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/1455770.1455828"},{"key":"ref7","first-page":"207","article-title":"Verified correctness and security of openssl hmac","author":"beringer","year":"2015","journal-title":"Proceedings of the 24th USENIX Conference on Security Symposium ser SEC’15"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103709"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.58"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500592"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.28"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806610"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429105"},{"key":"ref42","year":"2014","journal-title":"Cryptol"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/2527269.2527277"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.37"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_52"}],"event":{"name":"2019 IEEE\/ACM International Symposium on Code Generation and Optimization (CGO)","location":"Washington, DC, USA","start":{"date-parts":[[2019,2,16]]},"end":{"date-parts":[[2019,2,20]]}},"container-title":["2019 IEEE\/ACM International Symposium on Code Generation and Optimization (CGO)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8653576\/8661160\/08661180.pdf?arnumber=8661180","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,19]],"date-time":"2022-07-19T20:22:55Z","timestamp":1658262175000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8661180\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,2]]},"references-count":62,"URL":"https:\/\/doi.org\/10.1109\/cgo.2019.8661180","relation":{},"subject":[],"published":{"date-parts":[[2019,2]]}}}