Andres Erbsen

According to our database, Andres Erbsen authored at least 17 papers between 2018 and 2025.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2025

Securing Cryptographic Software via Typed Assembly Language (Extended Version).

Shixin Song, Tingzhen Dong, Kosi Nwabueze, Julian Zanders, Andres Erbsen, Adam Chlipala, Mengjia Yan

CoRR, September, 2025

Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers.

Owen Conoly, Andres Erbsen, Adam Chlipala

Proc. ACM Program. Lang., 2025

Securing Cryptographic Software via Typed Assembly Language.

Shixin Song, Tingzhen Dong, Kosi Nwabueze, Julian Zanders, Andres Erbsen, Adam Chlipala, Mengjia Yan

Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security, 2025

2024

Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq.

Jason Gross, Andres Erbsen, Jade Philipoom, Rajashree Agrawal, Adam Chlipala

J. Autom. Reason., September, 2024

Foundational Integration Verification of a Cryptographic Server.

Andres Erbsen, Jade Philipoom, Dustin Jamner, Ashley Lin, Samuel Gruetter, Clément Pit-Claudel, Adam Chlipala

Proc. ACM Program. Lang., 2024

2023

Flexible Instruction-Set Semantics via Abstract Monads (Experience Report).

Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Pratap Singh, Andy Wright, Adam Chlipala

Proc. ACM Program. Lang., August, 2023

Omnisemantics: Smooth Handling of Nondeterminism.

Arthur Charguéraud, Adam Chlipala, Andres Erbsen, Samuel Gruetter

ACM Trans. Program. Lang. Syst., March, 2023

CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives.

Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom

Proc. ACM Program. Lang., 2023

CryptOpt: Automatic Optimization of Straightline Code.

Joel Kuepper, David Wu, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom

Proceedings of the 45th IEEE/ACM International Conference on Software Engineering: ICSE 2023 Companion Proceedings, 2023

2022

Certifying derivation of state machines from coroutines.

Mirai Ikebuchi, Andres Erbsen, Adam Chlipala

Proc. ACM Program. Lang., 2022

CryptOpt: Verified Compilation with Random Program Search for Cryptographic Primitives.

Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom

CoRR, 2022

Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code.

Clément Pit-Claudel, Jade Philipoom, Dustin Jamner, Andres Erbsen, Adam Chlipala

Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

Accelerating Verified-Compiler Development with a Verified Rewriting Engine.

Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, Adam Chlipala

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

2021

A Multipurpose Formal RISC-V Specification.

Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Andrew Wright, Adam Chlipala

CoRR, 2021

Integration verification across software and hardware for a simple embedded system.

Andres Erbsen, Samuel Gruetter, Joonwon Choi, Clark Wood, Adam Chlipala

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

2019

Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises.

Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala

Proceedings of the 2019 IEEE Symposium on Security and Privacy, 2019

2018

Reification by Parametricity - Fast Setup for Proof by Reflection, in Two Lines of Ltac.

Jason Gross, Andres Erbsen, Adam Chlipala

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018