Andres Erbsen

23 papers A* 4B 3Journal 15Unranked 1
YearRankTypeTitle / Venue / Authors
2026 B conf
Foundational Verification of Running-Time Bounds for Interactive Programs.
CPP
Andy Tockman, Pratap Singh, Andres Erbsen, Samuel Gruetter, Adam Chlipala
2025 J jnl
Securing Cryptographic Software via Typed Assembly Language (Extended Version).
CoRR
Shixin Song, Tingzhen Dong, Kosi Nwabueze, Julian Zanders, Andres Erbsen, Adam Chlipala, Mengjia Yan
2025 A* conf
Securing Cryptographic Software via Typed Assembly Language.
CCS
Shixin Song, Tingzhen Dong, Kosi Nwabueze, Julian Zanders, Andres Erbsen, Adam Chlipala, Mengjia Yan
2025 J jnl
Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers.
CoRR
Owen Conoly, Andres Erbsen, Adam Chlipala
2025 J jnl
Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers.
Proc. ACM Program. Lang.
Owen Conoly, Andres Erbsen, Adam Chlipala
2024 J jnl
Foundational Integration Verification of a Cryptographic Server.
Proc. ACM Program. Lang.
Andres Erbsen, Jade Philipoom, Dustin Jamner, Ashley Lin, Samuel Gruetter, Clément Pit-Claudel, Adam Chlipala
2024 J jnl
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq.
J. Autom. Reason.
Jason Gross, Andres Erbsen, Jade Philipoom, Rajashree Agrawal, Adam Chlipala
2023 — conf
CryptOpt: Automatic Optimization of Straightline Code.
ICSE Companion
Joel Kuepper, David Wu, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
2023 J jnl
CryptOpt: Automatic Optimization of Straightline Code.
CoRR
Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
2023 J jnl
CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives.
Proc. ACM Program. Lang.
Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
2023 J jnl
Flexible Instruction-Set Semantics via Abstract Monads (Experience Report).
Proc. ACM Program. Lang.
Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Pratap Singh, Andy Wright, Adam Chlipala
2023 J jnl
Omnisemantics: Smooth Handling of Nondeterminism.
ACM Trans. Program. Lang. Syst.
Arthur Charguéraud, Adam Chlipala, Andres Erbsen, Samuel Gruetter
2023 J jnl
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq.
CoRR
Jason Gross, Andres Erbsen, Jade Philipoom, Rajashree Agrawal, Adam Chlipala
2022 B conf
Accelerating Verified-Compiler Development with a Verified Rewriting Engine.
ITP
Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, Adam Chlipala
2022 J jnl
Accelerating Verified-Compiler Development with a Verified Rewriting Engine.
CoRR
Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, Adam Chlipala
2022 J jnl
Certifying derivation of state machines from coroutines.
Proc. ACM Program. Lang.
Mirai Ikebuchi, Andres Erbsen, Adam Chlipala
2022 J jnl
CryptOpt: Verified Compilation with Random Program Search for Cryptographic Primitives.
CoRR
Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
2022 A* conf
Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code.
PLDI
Clément Pit-Claudel, Jade Philipoom, Dustin Jamner, Andres Erbsen, Adam Chlipala
2021 J jnl
A Multipurpose Formal RISC-V Specification.
CoRR
Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Andrew Wright, Adam Chlipala
2021 A* conf
Integration verification across software and hardware for a simple embedded system.
PLDI
Andres Erbsen, Samuel Gruetter, Joonwon Choi, Clark Wood, Adam Chlipala
2020 J jnl
Simple High-Level Code For Cryptographic Arithmetic: With Proofs, Without Compromises.
ACM SIGOPS Oper. Syst. Rev.
Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala
2019 A* conf
Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises.
IEEE Symposium on Security and Privacy
Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala
2018 B conf
Reification by Parametricity - Fast Setup for Proof by Reflection, in Two Lines of Ltac.
ITP
Jason Gross, Andres Erbsen, Adam Chlipala