{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T07:54:35Z","timestamp":1768031675188,"version":"3.49.0"},"reference-count":81,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"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":[[2023,6,6]]},"abstract":"<jats:p>Most software domains rely on compilers to translate high-level code to multiple different machine languages,  \nwith performance not too much worse than what developers would have the patience to write directly  \nin assembly language. However, cryptography has been an exception, where many performance-critical  \nroutines have been written directly in assembly (sometimes through metaprogramming layers). Some past  \nwork has shown how to do formal verification of that assembly, and other work has shown how to generate  \nC code automatically along with formal proof, but with consequent performance penalties vs. the best-  \nknown assembly. We present CryptOpt, the first compilation pipeline that specializes high-level cryptographic  \nfunctional programs into assembly code significantly faster than what GCC or Clang produce, with mechanized  \nproof (in Coq) whose final theorem statement mentions little beyond the input functional program and the  \noperational semantics of x86-64 assembly. On the optimization side, we apply randomized search through the  \nspace of assembly programs, with repeated automatic benchmarking on target CPUs. On the formal-verification  \nside, we connect to the Fiat Cryptography framework (which translates functional programs into C-like IR  \ncode) and extend it with a new formally verified program-equivalence checker, incorporating a modest subset  \nof known features of SMT solvers and symbolic-execution engines. The overall prototype is quite practical,  \ne.g. producing new fastest-known implementations of finite-field arithmetic for both Curve25519 (part of the  \nTLS standard) and the Bitcoin elliptic curve secp256k1 for the Intel 12\ud835\udc61\u210e and 13\ud835\udc61\u210e generations.<\/jats:p>","DOI":"10.1145\/3591272","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"1268-1292","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0643-2440","authenticated-orcid":false,"given":"Joel","family":"Kuepper","sequence":"first","affiliation":[{"name":"University of Adelaide, Australia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9854-7500","authenticated-orcid":false,"given":"Andres","family":"Erbsen","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9427-4891","authenticated-orcid":false,"given":"Jason","family":"Gross","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-3129-1218","authenticated-orcid":false,"given":"Owen","family":"Conoly","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-9226-3688","authenticated-orcid":false,"given":"Chuyue","family":"Sun","sequence":"additional","affiliation":[{"name":"Stanford University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-1906-5995","authenticated-orcid":false,"given":"Samuel","family":"Tian","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-7948-0604","authenticated-orcid":false,"given":"David","family":"Wu","sequence":"additional","affiliation":[{"name":"University of Adelaide, Australia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7085-9417","authenticated-orcid":false,"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0329-2681","authenticated-orcid":false,"given":"Chitchanok","family":"Chuengsatiansup","sequence":"additional","affiliation":[{"name":"University of Melbourne, Australia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2720-9288","authenticated-orcid":false,"given":"Daniel","family":"Genkin","sequence":"additional","affiliation":[{"name":"Georgia Institute of Technology, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3124-0061","authenticated-orcid":false,"given":"Markus","family":"Wagner","sequence":"additional","affiliation":[{"name":"Monash University, Australia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0401-4197","authenticated-orcid":false,"given":"Yuval","family":"Yarom","sequence":"additional","affiliation":[{"name":"Ruhr University Bochum, Germany"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Ullman","author":"Aho Alfred V.","year":"1986","unstructured":"Alfred V. Aho , Ravi Sethi , and Jeffrey D . Ullman . 1986 . Compilers : Principles, Techniques, and Tools. Addison-Wesley . Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. 1986. Compilers: Principles, Techniques, and Tools. Addison-Wesley."},{"key":"e_1_2_1_2_1","unstructured":"Jos\u00e9 Bacelar Almeida Manuel Barbosa Gilles Barthe Fran\u00e7ois Dupressoir and Michael Emmi. 2016. Verifying Constant-Time Implementations. In USENIX Security. 53\u201370. https:\/\/www.usenix.org\/conference\/usenixsecurity16\/technical-sessions\/presentation\/almeida \t\t\t\t  Jos\u00e9 Bacelar Almeida Manuel Barbosa Gilles Barthe Fran\u00e7ois Dupressoir and Michael Emmi. 2016. Verifying Constant-Time Implementations. In USENIX Security. 53\u201370. https:\/\/www.usenix.org\/conference\/usenixsecurity16\/technical-sessions\/presentation\/almeida"},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Micha\u00ebl Armand Germain Faure Benjamin Gr\u00e9goire Chantal Keller Laurent Th\u00e9ry and Benjamin Werner. 2011. A Modular Integration of SAT\/SMT Solvers to Coq through Proof Witnesses. In CPP. 135\u2013150. \t\t\t\t  Micha\u00ebl Armand Germain Faure Benjamin Gr\u00e9goire Chantal Keller Laurent Th\u00e9ry and Benjamin Werner. 2011. A Modular Integration of SAT\/SMT Solvers to Coq through Proof Witnesses. In CPP. 135\u2013150.","DOI":"10.1007\/978-3-642-25379-9_12"},{"key":"e_1_2_1_4_1","unstructured":"2011. Theory of Randomized Search Heuristics: Foundations and Recent Developments Anne Auger and Benjamin Doerr (Eds.) (Series on Theoretical Computer Science Vol. 1). World Scientific. \t\t\t\t  2011. Theory of Randomized Search Heuristics: Foundations and Recent Developments Anne Auger and Benjamin Doerr (Eds.) (Series on Theoretical Computer Science Vol. 1). World Scientific."},{"key":"e_1_2_1_5_1","volume-title":"Basil Hess, Amir Jalali, Brian Koziel, Brian LaMacchia, Patrick Longa, Michael Naehrig, Geovandro Pereira, Joost Renes, Vladimir Soukharev, and David Urbanik.","author":"Azarderakhsh Reza","year":"2019","unstructured":"Reza Azarderakhsh , Matthew Campagna , Craig Costello , Luca De Feo , Basil Hess, Amir Jalali, Brian Koziel, Brian LaMacchia, Patrick Longa, Michael Naehrig, Geovandro Pereira, Joost Renes, Vladimir Soukharev, and David Urbanik. 2019 . Supersingular Isogeny Key Encapsulation \u2013 Submission to the NIST Post-Quantum Standardization Project , round 2. https:\/\/sike.org Reza Azarderakhsh, Matthew Campagna, Craig Costello, Luca De Feo, Basil Hess, Amir Jalali, Brian Koziel, Brian LaMacchia, Patrick Longa, Michael Naehrig, Geovandro Pereira, Joost Renes, Vladimir Soukharev, and David Urbanik. 2019. Supersingular Isogeny Key Encapsulation \u2013 Submission to the NIST Post-Quantum Standardization Project, round 2. https:\/\/sike.org"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Sorav Bansal and Alex Aiken. 2006. Automatic generation of peephole superoptimizers. In ASPLOS. 394\u2013403. \t\t\t\t  Sorav Bansal and Alex Aiken. 2006. Automatic generation of peephole superoptimizers. In ASPLOS. 394\u2013403.","DOI":"10.1145\/1168918.1168906"},{"key":"e_1_2_1_7_1","first-page":"328","article-title":"Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic \u201cConstant-Time","author":"Barthe Gilles","year":"2018","unstructured":"Gilles Barthe , Benjamin Gr\u00e9goire , and Vincent Laporte . 2018 . Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic \u201cConstant-Time \u201d . In CSF. 328 \u2013 343 . Gilles Barthe, Benjamin Gr\u00e9goire, and Vincent Laporte. 2018. Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic \u201cConstant-Time\u201d. In CSF. 328\u2013343.","journal-title":". In CSF."},{"key":"e_1_2_1_8_1","volume-title":"Jes\u00fas-Javier Chi-Dom\u00ednguez, Luis Rivera-Zamarripa, and Igor Ustinov.","author":"Belyavsky Dmitry","year":"2020","unstructured":"Dmitry Belyavsky , Billy Bob Brumley , Jes\u00fas-Javier Chi-Dom\u00ednguez, Luis Rivera-Zamarripa, and Igor Ustinov. 2020 . Set It and Forget It! Turnkey ECC for Instant Integration. In ACSAC. 760\u2013771. Dmitry Belyavsky, Billy Bob Brumley, Jes\u00fas-Javier Chi-Dom\u00ednguez, Luis Rivera-Zamarripa, and Igor Ustinov. 2020. Set It and Forget It! Turnkey ECC for Instant Integration. In ACSAC. 760\u2013771."},{"key":"e_1_2_1_9_1","volume-title":"Encyclopedia of Information Systems. 141\u2013170.","author":"Bergmann Seth D.","unstructured":"Seth D. Bergmann . 2003. Compilers . In Encyclopedia of Information Systems. 141\u2013170. Seth D. Bergmann. 2003. Compilers. In Encyclopedia of Information Systems. 141\u2013170."},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Daniel J. Bernstein. 2005. The Poly1305-AES Message-Authentication Code. In FSE. 32\u201349. \t\t\t\t  Daniel J. Bernstein. 2005. The Poly1305-AES Message-Authentication Code. In FSE. 32\u201349.","DOI":"10.1007\/11502760_3"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Daniel J. Bernstein. 2006. Curve25519: New Diffie-Hellman Speed Records. In PKC. 207\u2013228. \t\t\t\t  Daniel J. Bernstein. 2006. Curve25519: New Diffie-Hellman Speed Records. In PKC. 207\u2013228.","DOI":"10.1007\/11745853_14"},{"key":"e_1_2_1_12_1","first-page":"250","article-title":"McBits: Fast Constant-Time Code-Based Cryptography","volume":"8086","author":"Bernstein Daniel J.","year":"2013","unstructured":"Daniel J. Bernstein , Tung Chou , and Peter Schwabe . 2013 . McBits: Fast Constant-Time Code-Based Cryptography . In CHES. 8086 , 250 \u2013 272 . Daniel J. Bernstein, Tung Chou, and Peter Schwabe. 2013. McBits: Fast Constant-Time Code-Based Cryptography. In CHES. 8086, 250\u2013272.","journal-title":"CHES."},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Daniel J. Bernstein Chitchanok Chuengsatiansup and Tanja Lange. 2014. Curve41417: Karatsuba Revisited. In CHES. 316\u2013334. \t\t\t\t  Daniel J. Bernstein Chitchanok Chuengsatiansup and Tanja Lange. 2014. Curve41417: Karatsuba Revisited. In CHES. 316\u2013334.","DOI":"10.1007\/978-3-662-44709-3_18"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Daniel J. Bernstein Chitchanok Chuengsatiansup Tanja Lange and Peter Schwabe. 2014. Kummer Strikes Back: New DH Speed Records. In ASIACRYPT. 317\u2013337. \t\t\t\t  Daniel J. Bernstein Chitchanok Chuengsatiansup Tanja Lange and Peter Schwabe. 2014. Kummer Strikes Back: New DH Speed Records. In ASIACRYPT. 317\u2013337.","DOI":"10.1007\/978-3-662-45611-8_17"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Daniel J. Bernstein Chitchanok Chuengsatiansup Tanja Lange and Christine van Vredendaal. 2017. NTRU Prime: Reducing Attack Surface at Low Cost. In SAC. 235\u2013260. \t\t\t\t  Daniel J. Bernstein Chitchanok Chuengsatiansup Tanja Lange and Christine van Vredendaal. 2017. NTRU Prime: Reducing Attack Surface at Low Cost. In SAC. 235\u2013260.","DOI":"10.1007\/978-3-319-72565-9_12"},{"key":"e_1_2_1_16_1","volume-title":"Bernstein and Tanja Lange","author":"Daniel","year":"2022","unstructured":"Daniel J. Bernstein and Tanja Lange . 2022 . eBACS: ECRYPT benchmarking of cryptographic systems. http:\/\/bench.cr.yp.to\/supercop\/supercop-20221005.tar.xz Daniel J. Bernstein and Tanja Lange. 2022. eBACS: ECRYPT benchmarking of cryptographic systems. http:\/\/bench.cr.yp.to\/supercop\/supercop-20221005.tar.xz"},{"key":"e_1_2_1_17_1","volume-title":"Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate","author":"Bhargavan Karthikeyan","unstructured":"Karthikeyan Bhargavan , Bruno Blanchet , and Nadim Kobeissi . 2017. Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate . In IEEE SP. 483\u2013502. Karthikeyan Bhargavan, Bruno Blanchet, and Nadim Kobeissi. 2017. Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. In IEEE SP. 483\u2013502."},{"key":"e_1_2_1_18_1","volume-title":"Proc. SNAPL. https:\/\/project-everest.github.io\/assets\/snapl2017","author":"Bhargavan Karthikeyan","year":"2017","unstructured":"Karthikeyan Bhargavan , Barry Bond , Antoine Delignat-Lavaud , C\u00e9dric Fournet , Chris Hawblitzel , Catalin Hritcu , Samin Ishtiaq , Markulf Kohlweiss , Rustan Leino , Jay Lorch , Kenji Maillard , Jianyang Pang , Bryan Parno , Jonathan Protzenko , Tahina Ramananandro , Ashay Rane , Aseem Rastogi , Nikhil Swamy , Laure Thompson , Peng Wang , Santiago Zanella-B\u00e9guelin , and Jean-Karim Zinzindohou\u00e9 . 2017 . Everest: Towards a Verified and Drop-in Replacement of HTTPS . In Proc. SNAPL. https:\/\/project-everest.github.io\/assets\/snapl2017 .pdf Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jianyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-B\u00e9guelin, and Jean-Karim Zinzindohou\u00e9. 2017. Everest: Towards a Verified and Drop-in Replacement of HTTPS. In Proc. SNAPL. https:\/\/project-everest.github.io\/assets\/snapl2017.pdf"},{"key":"e_1_2_1_19_1","unstructured":"Bitcoin Core. 2021. libsecp256k1 - Optimized C Library for ECDSA Signatures and Secret\/Public Key Operations on Curve secp256k1. https:\/\/github.com\/bitcoin-core\/secp256k1\/blob\/9526874d1406a13193743c605ba64358d55a8785\/src\/field_5x52_int128_impl.h \t\t\t\t  Bitcoin Core. 2021. libsecp256k1 - Optimized C Library for ECDSA Signatures and Secret\/Public Key Operations on Curve secp256k1. https:\/\/github.com\/bitcoin-core\/secp256k1\/blob\/9526874d1406a13193743c605ba64358d55a8785\/src\/field_5x52_int128_impl.h"},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Jay Bosamiya Sydney Gibson Yao Li Bryan Parno and Chris Hawblitzel. 2020. Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language. In VSTTE. 106\u2013123. \t\t\t\t  Jay Bosamiya Sydney Gibson Yao Li Bryan Parno and Chris Hawblitzel. 2020. Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language. In VSTTE. 106\u2013123.","DOI":"10.1007\/978-3-030-63618-0_7"},{"key":"e_1_2_1_21_1","unstructured":"Christopher Celio Palmer Dabbelt David A. Patterson and Krste Asanovic. 2016. The Renewed Case for the Reduced Instruction Set Computer: Avoiding ISA Bloat with Macro-Op Fusion for RISC-V. arXiv 1607.02318. \t\t\t\t  Christopher Celio Palmer Dabbelt David A. Patterson and Krste Asanovic. 2016. The Renewed Case for the Reduced Instruction Set Computer: Avoiding ISA Bloat with Macro-Op Fusion for RISC-V. arXiv 1607.02318."},{"key":"e_1_2_1_22_1","unstructured":"Certicom Research. 2000. SEC 2: Recommended elliptic curve domain parameters version 1.0.  http:\/\/www.secg.org\/SEC2-Ver-1.0.pdf \t\t\t\t  Certicom Research. 2000. SEC 2: Recommended elliptic curve domain parameters version 1.0.  http:\/\/www.secg.org\/SEC2-Ver-1.0.pdf"},{"key":"e_1_2_1_23_1","volume-title":"Rabbah","author":"Chakrapani Lakshmi N.","year":"2005","unstructured":"Lakshmi N. Chakrapani , John Gyllenhaal , Wen-mei W. Hwu , Scott A. Mahlke , Krishna V. Palem , and Rodric M . Rabbah . 2005 . Trimaran : An Infrastructure for Research in Instruction-Level Parallelism. In Languages and Compilers for High Performance Computing . 32\u201341. Lakshmi N. Chakrapani, John Gyllenhaal, Wen-mei W. Hwu, Scott A. Mahlke, Krishna V. Palem, and Rodric M. Rabbah. 2005. Trimaran: An Infrastructure for Research in Instruction-Level Parallelism. In Languages and Compilers for High Performance Computing. 32\u201341."},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Yu-Fang Chen Chang-Hong Hsu Hsin-Hung Lin Peter Schwabe Ming-Hsien Tsai Bow-Yaw Wang Bo-Yin Yang and Shang-Yi Yang. 2014. Verifying Curve25519 Software. In CCS. 299\u2013309. \t\t\t\t  Yu-Fang Chen Chang-Hong Hsu Hsin-Hung Lin Peter Schwabe Ming-Hsien Tsai Bow-Yaw Wang Bo-Yin Yang and Shang-Yi Yang. 2014. Verifying Curve25519 Software. In CCS. 299\u2013309.","DOI":"10.1145\/2660267.2660370"},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Tung Chou. 2015. Sandy2x: New Curve25519 Speed Records. In SAC. 145\u2013160. \t\t\t\t  Tung Chou. 2015. Sandy2x: New Curve25519 Speed Records. In SAC. 145\u2013160.","DOI":"10.1007\/978-3-319-31301-6_8"},{"key":"e_1_2_1_26_1","first-page":"280","article-title":"QcBits: Constant-Time Small-Key Code-Based Cryptography","volume":"9813","author":"Chou Tung","year":"2016","unstructured":"Tung Chou . 2016 . QcBits: Constant-Time Small-Key Code-Based Cryptography . In CHES. 9813 , 280 \u2013 300 . Tung Chou. 2016. QcBits: Constant-Time Small-Key Code-Based Cryptography. In CHES. 9813, 280\u2013300.","journal-title":"CHES."},{"key":"e_1_2_1_27_1","first-page":"229","article-title":"PandA","volume":"8365","author":"Chuengsatiansup Chitchanok","year":"2013","unstructured":"Chitchanok Chuengsatiansup , Michael Naehrig , Pance Ribarski , and Peter Schwabe . 2013 . PandA : Pairings and Arithmetic. In Pairing. 8365 , 229 \u2013 250 . Chitchanok Chuengsatiansup, Michael Naehrig, Pance Ribarski, and Peter Schwabe. 2013. PandA: Pairings and Arithmetic. In Pairing. 8365, 229\u2013250.","journal-title":"Pairings and Arithmetic. In Pairing."},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Chitchanok Chuengsatiansup and Damien Stehl\u00e9. 2019. Towards Practical GGM-Based PRF from (Module-) Learning-with-Rounding. In SAC. 693\u2013713. \t\t\t\t  Chitchanok Chuengsatiansup and Damien Stehl\u00e9. 2019. Towards Practical GGM-Based PRF from (Module-) Learning-with-Rounding. In SAC. 693\u2013713.","DOI":"10.1007\/978-3-030-38471-5_28"},{"key":"e_1_2_1_29_1","unstructured":"Clang. 2022. Clang: a C language family frontend for LLVM. https:\/\/clang.llvm.org \t\t\t\t  Clang. 2022. Clang: a C language family frontend for LLVM. https:\/\/clang.llvm.org"},{"key":"e_1_2_1_30_1","volume-title":"Cooper and Linda Torczon","author":"Keith","year":"2012","unstructured":"Keith D. Cooper and Linda Torczon . 2012 . Chapter 11 - Instruction Selection. In Engineering a Compiler (Second Edition) . 597\u2013638. Keith D. Cooper and Linda Torczon. 2012. Chapter 11 - Instruction Selection. In Engineering a Compiler (Second Edition). 597\u2013638."},{"key":"e_1_2_1_31_1","volume-title":"Bj\u00f8rner","author":"de Moura Leonardo Mendon\u00e7a","year":"2008","unstructured":"Leonardo Mendon\u00e7a de Moura and Nikolaj S . Bj\u00f8rner . 2008 . Z3: An Efficient SMT Solver. In TACAS. 337\u2013340. Leonardo Mendon\u00e7a de Moura and Nikolaj S. Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS. 337\u2013340."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_2_1_33_1","volume-title":"Theory of evolutionary computation: Recent developments in discrete optimization","author":"Doerr Benjamin","unstructured":"Benjamin Doerr and Frank Neumann . 2019. Theory of evolutionary computation: Recent developments in discrete optimization . Springer . Benjamin Doerr and Frank Neumann. 2019. Theory of evolutionary computation: Recent developments in discrete optimization. Springer."},{"key":"e_1_2_1_34_1","volume-title":"The Correctness-Security Gap in Compiler Optimization. In IEEE SP Workshops. 73\u201387","author":"D\u2019Silva Vijay","year":"2015","unstructured":"Vijay D\u2019Silva , Mathias Payer , and Dawn Xiaodong Song . 2015 . The Correctness-Security Gap in Compiler Optimization. In IEEE SP Workshops. 73\u201387 . Vijay D\u2019Silva, Mathias Payer, and Dawn Xiaodong Song. 2015. The Correctness-Security Gap in Compiler Optimization. In IEEE SP Workshops. 73\u201387."},{"key":"e_1_2_1_35_1","volume-title":"Without Compromises","author":"Erbsen Andres","unstructured":"Andres Erbsen , Jade Philipoom , Jason Gross , Robert Sloan , and Adam Chlipala . 2019. Simple High-Level Code for Cryptographic Arithmetic - With Proofs , Without Compromises . In IEEE SP. 1202\u20131219. Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. 2019. Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises. In IEEE SP. 1202\u20131219."},{"key":"e_1_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Jean-Christophe Filli\u00e2tre and Andrei Paskevich. 2013. Why3 - Where Programs Meet Provers. In ESOP. 125\u2013128. \t\t\t\t  Jean-Christophe Filli\u00e2tre and Andrei Paskevich. 2013. Why3 - Where Programs Meet Provers. In ESOP. 125\u2013128.","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1287\/opre.2013.1231"},{"key":"e_1_2_1_38_1","first-page":"1","article-title":"A verified, efficient embedding of a verifiable assembly language","volume":"63","author":"Fromherz Aymeric","year":"2019","unstructured":"Aymeric Fromherz , Nick Giannarakis , Chris Hawblitzel , Bryan Parno , Aseem Rastogi , and Nikhil Swamy . 2019 . A verified, efficient embedding of a verifiable assembly language . In POPL. 63 : 1 \u2013 63 :30. Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, and Nikhil Swamy. 2019. A verified, efficient embedding of a verifiable assembly language. In POPL. 63:1\u201363:30.","journal-title":"POPL."},{"key":"e_1_2_1_39_1","doi-asserted-by":"crossref","unstructured":"Yu-Fu Fu Jiaxiang Liu Xiaomu Shi Ming-Hsien Tsai Bow-Yaw Wang and Bo-Yin Yang. 2019. Signed Cryptographic Program Verification with Typed CryptoLine. In CCS. ACM 1591\u20131606. \t\t\t\t  Yu-Fu Fu Jiaxiang Liu Xiaomu Shi Ming-Hsien Tsai Bow-Yaw Wang and Bo-Yin Yang. 2019. Signed Cryptographic Program Verification with Typed CryptoLine. In CCS. ACM 1591\u20131606.","DOI":"10.1145\/3319535.3354199"},{"key":"e_1_2_1_40_1","unstructured":"GCC. 2022. GCC the GNU Compiler Collection. https:\/\/gcc.gnu.org \t\t\t\t  GCC. 2022. GCC the GNU Compiler Collection. https:\/\/gcc.gnu.org"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13389-016-0141-6"},{"key":"e_1_2_1_42_1","unstructured":"HACL. 2022. HACL. https:\/\/github.com\/hacl-star\/hacl-star \t\t\t\t  HACL. 2022. HACL. https:\/\/github.com\/hacl-star\/hacl-star"},{"key":"e_1_2_1_43_1","first-page":"625","article-title":"Ed448-Goldilocks, a new elliptic curve","volume":"2015","author":"Hamburg Mike","year":"2015","unstructured":"Mike Hamburg . 2015 . Ed448-Goldilocks, a new elliptic curve . IACR Cryptology ePrint Archive , 2015 (2015), 625 . Mike Hamburg. 2015. Ed448-Goldilocks, a new elliptic curve. IACR Cryptology ePrint Archive, 2015 (2015), 625.","journal-title":"IACR Cryptology ePrint Archive"},{"key":"e_1_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Saemundur O. Haraldsson John R. Woodward Alexander E. I. Brownlee and Kristin Siggeirsdottir. 2017. Fixing bugs in your sleep: how genetic improvement became an overnight success. In GECCO (Companion). 1513\u20131520. \t\t\t\t  Saemundur O. Haraldsson John R. Woodward Alexander E. I. Brownlee and Kristin Siggeirsdottir. 2017. Fixing bugs in your sleep: how genetic improvement became an overnight success. In GECCO (Companion). 1513\u20131520.","DOI":"10.1145\/3067695.3082517"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(01)00196-3"},{"key":"e_1_2_1_46_1","volume-title":"Hooker and Collin Eddy","author":"Rodney","year":"2013","unstructured":"Rodney E. Hooker and Collin Eddy . 2013 . Store-to-load forwarding based on load\/store address computation source information comparisons. US Patent 8533438. Rodney E. Hooker and Collin Eddy. 2013. Store-to-load forwarding based on load\/store address computation source information comparisons. US Patent 8533438."},{"key":"e_1_2_1_47_1","volume-title":"Randall","author":"Joshi Rajeev","year":"2002","unstructured":"Rajeev Joshi , Greg Nelson , and Keith H . Randall . 2002 . Denali : A Goal-directed Superoptimizer. In PLDI. ACM , 304\u2013314. Rajeev Joshi, Greg Nelson, and Keith H. Randall. 2002. Denali: A Goal-directed Superoptimizer. In PLDI. ACM, 304\u2013314."},{"key":"e_1_2_1_48_1","doi-asserted-by":"crossref","unstructured":"Matthias J. Kannwischer Joost Rijneveld and Peter Schwabe. 2019. Faster Multiplication in Z_2^m[x] on Cortex-M4 to Speed up NIST PQC Candidates. In ACNS. 281\u2013301. \t\t\t\t  Matthias J. Kannwischer Joost Rijneveld and Peter Schwabe. 2019. Faster Multiplication in Z_2^m[x] on Cortex-M4 to Speed up NIST PQC Candidates. In ACNS. 281\u2013301.","DOI":"10.1007\/978-3-030-21568-2_14"},{"key":"e_1_2_1_49_1","volume-title":"When Constant-Time Source Yields Variable-Time Binary: Exploiting Curve25519-donna Built with MSVC","author":"Kaufmann Thierry","year":"2015","unstructured":"Thierry Kaufmann , Herv\u00e9 Pelletier , Serge Vaudenay , and Karine Villegas . 2016. When Constant-Time Source Yields Variable-Time Binary: Exploiting Curve25519-donna Built with MSVC 2015 . In CANS. 573\u2013582. Thierry Kaufmann, Herv\u00e9 Pelletier, Serge Vaudenay, and Karine Villegas. 2016. When Constant-Time Source Yields Variable-Time Binary: Exploiting Curve25519-donna Built with MSVC 2015. In CANS. 573\u2013582."},{"key":"e_1_2_1_50_1","volume-title":"Justyna Petke, and Mark Harman.","author":"Langdon William B.","year":"2015","unstructured":"William B. Langdon , Brian Yee Hong Lam , Justyna Petke, and Mark Harman. 2015 . Improving CUDA DNA Analysis Software with Genetic Programming. In GECCO. 1063\u20131070. William B. Langdon, Brian Yee Hong Lam, Justyna Petke, and Mark Harman. 2015. Improving CUDA DNA Analysis Software with Genetic Programming. In GECCO. 1063\u20131070."},{"key":"e_1_2_1_51_1","unstructured":"Adam Langley. 2022. Curve25519-donna. https:\/\/github.com\/agl\/curve25519-donna \t\t\t\t  Adam Langley. 2022. Curve25519-donna. https:\/\/github.com\/agl\/curve25519-donna"},{"key":"e_1_2_1_52_1","volume-title":"Lipasti","author":"Lepak Kevin M.","year":"2000","unstructured":"Kevin M. Lepak and Mikko H . Lipasti . 2000 . On the value locality of store instructions. In ISCA. 182\u2013191. Kevin M. Lepak and Mikko H. Lipasti. 2000. On the value locality of store instructions. In ISCA. 182\u2013191."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_2_1_54_1","unstructured":"Xavier Leroy Sandrine Blazy Daniel K\u00e4stner Bernhard Schommer Markus Pister and Christian Ferdinand. 2016. CompCert \u2014 A Formally Verified Optimizing Compiler. In ERTS. \t\t\t\t  Xavier Leroy Sandrine Blazy Daniel K\u00e4stner Bernhard Schommer Markus Pister and Christian Ferdinand. 2016. CompCert \u2014 A Formally Verified Optimizing Compiler. In ERTS."},{"key":"e_1_2_1_55_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 PLDI. 65\u201379. \t\t\t\t  Nuno P. Lopes Juneyoung Lee Chung-Kil Hur Zhengyang Liu and John Regehr. 2021. Alive2: bounded translation validation for LLVM. In PLDI. 65\u201379.","DOI":"10.1145\/3453483.3454030"},{"key":"e_1_2_1_56_1","volume-title":"Superoptimizer - A Look at the Smallest Program","author":"Massalin Henry","unstructured":"Henry Massalin . 1987. Superoptimizer - A Look at the Smallest Program . In ASPLOS. ACM Press , 122\u2013126. Henry Massalin. 1987. Superoptimizer - A Look at the Smallest Program. In ASPLOS. ACM Press, 122\u2013126."},{"key":"e_1_2_1_57_1","unstructured":"NIST. 2000. FIPS PUB 186-2: Digital signature standard. \t\t\t\t  NIST. 2000. FIPS PUB 186-2: Digital signature standard."},{"key":"e_1_2_1_58_1","unstructured":"OpenSSL. 2022. OpenSSL. https:\/\/www.openssl.org\/ \t\t\t\t  OpenSSL. 2022. OpenSSL. https:\/\/www.openssl.org\/"},{"key":"e_1_2_1_59_1","volume-title":"Andrew N. Sloss, Kenneth N. Reid, Yuan Yuan, and Wolfgang Banzhaf.","author":"Peeler Hannah","year":"2022","unstructured":"Hannah Peeler , Shuyue Stella Li , Andrew N. Sloss, Kenneth N. Reid, Yuan Yuan, and Wolfgang Banzhaf. 2022 . Optimizing LLVM Pass Sequences with Shackleton : A Linear Genetic Programming Framework . arXiv 2201.13305. Hannah Peeler, Shuyue Stella Li, Andrew N. Sloss, Kenneth N. Reid, Yuan Yuan, and Wolfgang Banzhaf. 2022. Optimizing LLVM Pass Sequences with Shackleton: A Linear Genetic Programming Framework. arXiv 2201.13305."},{"key":"e_1_2_1_60_1","volume-title":"Software Automatic Tuning, From Concepts to State-of-the-Art Results","author":"Pekhimenko Gennady","unstructured":"Gennady Pekhimenko and Angela Demke Brown . 2010. Efficient Program Compilation Through Machine Learning Techniques . In Software Automatic Tuning, From Concepts to State-of-the-Art Results . Springer , 335\u2013351. Gennady Pekhimenko and Angela Demke Brown. 2010. Efficient Program Compilation Through Machine Learning Techniques. In Software Automatic Tuning, From Concepts to State-of-the-Art Results. Springer, 335\u2013351."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/TEVC.2017.2693219"},{"key":"e_1_2_1_62_1","doi-asserted-by":"crossref","unstructured":"Amir Pnueli Michael Siegel and Eli Singerman. 1998. Translation Validation. In TACAS. 151\u2013166. \t\t\t\t  Amir Pnueli Michael Siegel and Eli Singerman. 1998. Translation Validation. In TACAS. 151\u2013166.","DOI":"10.1007\/BFb0054170"},{"key":"e_1_2_1_63_1","first-page":"1","article-title":"Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk). In CONCUR (LIPIcs, Vol. 118)","volume":"4","author":"Polyakov Andy","year":"2018","unstructured":"Andy Polyakov , Ming-Hsien Tsai , Bow-Yaw Wang , and Bo-Yin Yang . 2018 . Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk). In CONCUR (LIPIcs, Vol. 118) . Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik , 4 : 1 \u2013 4 :16. Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. 2018. Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk). In CONCUR (LIPIcs, Vol. 118). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 4:1\u20134:16.","journal-title":"Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik"},{"key":"e_1_2_1_64_1","volume-title":"Verified, Cross-Platform Cryptographic Provider","author":"Protzenko Jonathan","unstructured":"Jonathan Protzenko , Bryan Parno , Aymeric Fromherz , Chris Hawblitzel , Marina Polubelova , Karthikeyan Bhargavan , Benjamin Beurdouche , Joonwon Choi , Antoine Delignat-Lavaud , C\u00e9dric Fournet , Natalia Kulatova , Tahina Ramananandro , Aseem Rastogi , Nikhil Swamy , Christoph M. Wintersteiger , and Santiago Zanella B\u00e9guelin . 2020. EverCrypt : A Fast , Verified, Cross-Platform Cryptographic Provider . In IEEE SP. 983\u20131002. Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, and Santiago Zanella B\u00e9guelin. 2020. EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. In IEEE SP. 983\u20131002."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00060"},{"key":"e_1_2_1_67_1","volume-title":"Separation Logic: A Logic for Shared Mutable Data Structures. In LICS.","author":"Reynolds John C.","year":"2002","unstructured":"John C. Reynolds . 2002 . Separation Logic: A Logic for Shared Mutable Data Structures. In LICS. John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS."},{"key":"e_1_2_1_68_1","unstructured":"Ronny Ronen Alexander Peleg and Nathaniel Hoffman. 2004. System and method for fusing instructions. US Patent 6675376B2. \t\t\t\t  Ronny Ronen Alexander Peleg and Nathaniel Hoffman. 2004. System and method for fusing instructions. US Patent 6675376B2."},{"key":"e_1_2_1_69_1","volume-title":"Souper: A Synthesizing Superoptimizer. CoRR, abs\/1711.04422","author":"Sasnauskas Raimondas","year":"2017","unstructured":"Raimondas Sasnauskas , Yang Chen , Peter Collingbourne , Jeroen Ketema , Jubi Taneja , and John Regehr . 2017 . Souper: A Synthesizing Superoptimizer. CoRR, abs\/1711.04422 (2017). Raimondas Sasnauskas, Yang Chen, Peter Collingbourne, Jeroen Ketema, Jubi Taneja, and John Regehr. 2017. Souper: A Synthesizing Superoptimizer. CoRR, abs\/1711.04422 (2017)."},{"key":"e_1_2_1_70_1","doi-asserted-by":"crossref","unstructured":"Eric Schkufza Rahul Sharma and Alex Aiken. 2013. Stochastic superoptimization. In ASPLOS. ACM 305\u2013316. \t\t\t\t  Eric Schkufza Rahul Sharma and Alex Aiken. 2013. Stochastic superoptimization. In ASPLOS. ACM 305\u2013316.","DOI":"10.1145\/2490301.2451150"},{"key":"e_1_2_1_71_1","doi-asserted-by":"crossref","unstructured":"Eric Schkufza Rahul Sharma and Alex Aiken. 2014. Stochastic optimization of floating-point programs with tunable precision. In PLDI. ACM 53\u201364. \t\t\t\t  Eric Schkufza Rahul Sharma and Alex Aiken. 2014. Stochastic optimization of floating-point programs with tunable precision. In PLDI. ACM 53\u201364.","DOI":"10.1145\/2666356.2594302"},{"key":"e_1_2_1_72_1","volume-title":"van Eekelen","author":"Schoolderman Marc","year":"2021","unstructured":"Marc Schoolderman , Jonathan Moerman , Sjaak Smetsers , and Marko C. J. D . van Eekelen . 2021 . Efficient Verification of Optimized Code - Correct High-Speed X25519. In NFM. 304\u2013321. Marc Schoolderman, Jonathan Moerman, Sjaak Smetsers, and Marko C. J. D. van Eekelen. 2021. Efficient Verification of Optimized Code - Correct High-Speed X25519. In NFM. 304\u2013321."},{"key":"e_1_2_1_73_1","doi-asserted-by":"crossref","unstructured":"Thomas Arthur Leck Sewell Magnus O. Myreen and Gerwin Klein. 2013. Translation validation for a verified OS kernel. In PLDI. 471\u2013482. \t\t\t\t  Thomas Arthur Leck Sewell Magnus O. Myreen and Gerwin Klein. 2013. Translation validation for a verified OS kernel. In PLDI. 471\u2013482.","DOI":"10.1145\/2499370.2462183"},{"key":"e_1_2_1_74_1","doi-asserted-by":"crossref","unstructured":"Rahul Sharma Eric Schkufza Berkeley R. Churchill and Alex Aiken. 2013. Data-driven equivalence checking. In OOPSLA. ACM 391\u2013406. \t\t\t\t  Rahul Sharma Eric Schkufza Berkeley R. Churchill and Alex Aiken. 2013. Data-driven equivalence checking. In OOPSLA. ACM 391\u2013406.","DOI":"10.1145\/2544173.2509509"},{"key":"e_1_2_1_75_1","doi-asserted-by":"crossref","unstructured":"Rahul Sharma Eric Schkufza Berkeley R. Churchill and Alex Aiken. 2015. Conditionally correct superoptimization. In OOPSLA. ACM 147\u2013162. \t\t\t\t  Rahul Sharma Eric Schkufza Berkeley R. Churchill and Alex Aiken. 2015. Conditionally correct superoptimization. In OOPSLA. ACM 147\u2013162.","DOI":"10.1145\/2858965.2814278"},{"key":"e_1_2_1_76_1","volume-title":"Amarasinghe","author":"Stephenson Mark","year":"2003","unstructured":"Mark Stephenson , Una-May O\u2019Reilly , Martin C. Martin , and Saman P . Amarasinghe . 2003 . Genetic Programming Applied to Compiler Heuristic Optimization. In EuroGP. 238\u2013253. Mark Stephenson, Una-May O\u2019Reilly, Martin C. Martin, and Saman P. Amarasinghe. 2003. Genetic Programming Applied to Compiler Heuristic Optimization. In EuroGP. 238\u2013253."},{"key":"e_1_2_1_77_1","volume-title":"Loh","author":"Subramaniam Samantika","year":"2006","unstructured":"Samantika Subramaniam and Gabriel H . Loh . 2006 . Fire-and-Forget: Load\/ Store Scheduling with No Store Queue at All. In MICRO. 273\u2013284. Samantika Subramaniam and Gabriel H. Loh. 2006. Fire-and-Forget: Load\/Store Scheduling with No Store Queue at All. In MICRO. 273\u2013284."},{"key":"e_1_2_1_78_1","doi-asserted-by":"crossref","unstructured":"Jean-Baptiste Tristan and Xavier Leroy. 2008. Formal verification of translation validators: a case study on instruction scheduling optimizations. In POPL. 17\u201327. \t\t\t\t  Jean-Baptiste Tristan and Xavier Leroy. 2008. Formal verification of translation validators: a case study on instruction scheduling optimizations. In POPL. 17\u201327.","DOI":"10.1145\/1328897.1328444"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134076"},{"key":"e_1_2_1_80_1","doi-asserted-by":"crossref","unstructured":"Pepe Vila Pierre Ganty Marco Guarnieri and Boris K\u00f6pf. 2020. CacheQuery: learning replacement policies from hardware caches. In PLDI. 519\u2013532. \t\t\t\t  Pepe Vila Pierre Ganty Marco Guarnieri and Boris K\u00f6pf. 2020. CacheQuery: learning replacement policies from hardware caches. In PLDI. 519\u2013532.","DOI":"10.1145\/3385412.3386008"},{"key":"e_1_2_1_81_1","doi-asserted-by":"crossref","unstructured":"Thomas Weise Zijun Wu and Markus Wagner. 2019. An Improved Generic Bet-and-Run Strategy with Performance Prediction for Stochastic Local Search. In AAAI. 2395\u20132402. \t\t\t\t  Thomas Weise Zijun Wu and Markus Wagner. 2019. An Improved Generic Bet-and-Run Strategy with Performance Prediction for Stochastic Local Search. In AAAI. 2395\u20132402.","DOI":"10.1609\/aaai.v33i01.33012395"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591272","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591272","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591272","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:20Z","timestamp":1750178840000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591272"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":81,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591272"],"URL":"https:\/\/doi.org\/10.1145\/3591272","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}