Andres Erbsen

Publication Activity (10 Years)

Years Active: 2018-2024
Publications (10 Years): 18

Top Topics

Presburger Arithmetic

Instruction Set Architecture

Top Venues

Proc. ACM Program. Lang.

Publications

Jason Gross, Andres Erbsen, Jade Philipoom, Rajashree Agrawal, Adam Chlipala
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq. J. Autom. Reason. 68 (3) (2024)
Andres Erbsen, Jade Philipoom, Dustin Jamner, Ashley Lin, Samuel Gruetter, Clément Pit-Claudel, Adam Chlipala
Foundational Integration Verification of a Cryptographic Server. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Joel Kuepper, David Wu, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
CryptOpt: Automatic Optimization of Straightline Code. ICSE Companion (2023)
Arthur Charguéraud, Adam Chlipala, Andres Erbsen, Samuel Gruetter
Omnisemantics: Smooth Handling of Nondeterminism. ACM Trans. Program. Lang. Syst. 45 (1) (2023)
Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
CryptOpt: Automatic Optimization of Straightline Code. CoRR (2023)
Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Pratap Singh, Andy Wright, Adam Chlipala
Flexible Instruction-Set Semantics via Abstract Monads (Experience Report). Proc. ACM Program. Lang. 7 (ICFP) (2023)
Jason Gross, Andres Erbsen, Jade Philipoom, Rajashree Agrawal, Adam Chlipala
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq. CoRR (2023)
Mirai Ikebuchi, Andres Erbsen, Adam Chlipala
Certifying derivation of state machines from coroutines. Proc. ACM Program. Lang. 6 (POPL) (2022)
Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, Adam Chlipala
Accelerating Verified-Compiler Development with a Verified Rewriting Engine. CoRR (2022)
Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
CryptOpt: Verified Compilation with Random Program Search for Cryptographic Primitives. CoRR (2022)
Clément Pit-Claudel, Jade Philipoom, Dustin Jamner, Andres Erbsen, Adam Chlipala
Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code. PLDI (2022)
Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, Adam Chlipala
Accelerating Verified-Compiler Development with a Verified Rewriting Engine. ITP (2022)
Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Andrew Wright, Adam Chlipala
A Multipurpose Formal RISC-V Specification. CoRR (2021)
Andres Erbsen, Samuel Gruetter, Joonwon Choi, Clark Wood, Adam Chlipala
Integration verification across software and hardware for a simple embedded system. PLDI (2021)
Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala
Simple High-Level Code For Cryptographic Arithmetic: With Proofs, Without Compromises. ACM SIGOPS Oper. Syst. Rev. 54 (1) (2020)
Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala
Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises. IEEE Symposium on Security and Privacy (2019)
Jason Gross, Andres Erbsen, Adam Chlipala
Reification by Parametricity - Fast Setup for Proof by Reflection, in Two Lines of Ltac. ITP (2018)