Follow
Andres Erbsen
Andres Erbsen
MIT CSAIL
Verified email at mit.edu - Homepage
Title
Cited by
Cited by
Year
Simple High-Level Code For Cryptographic Arithmetic: With Proofs, Without Compromises
A Erbsen, J Philipoom, J Gross, R Sloan, A Chlipala
ACM SIGOPS Operating Systems Review 54 (1), 23-30, 2020
1632020
Integration Verification Across Software and Hardware for a Simple Embedded System
A Erbsen, S Gruetter, J Choi, C Wood, A Chlipala
42nd ACM SIGPLAN Conference on Programming Language Design and …, 2021
592021
Flexible Instruction-Set Semantics via Abstract Monads (Experience Report)
T Bourgeat, I Clester, A Erbsen, S Gruetter, P Singh, A Wright, A Chlipala
Proceedings of the ACM on Programming Languages 7 (ICFP), 108-124, 2023
25*2023
Relational compilation for performance-critical applications
C Pit-Claudel, J Philipoom, D Jamner, A Erbsen, A Chlipala
ACM| Proceedings of the 43rd ACM SIGPLAN International Conference on …, 2022
16*2022
CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives (full version)
J Kuepper, A Erbsen, J Gross, O Conoly, C Sun, S Tian, D Wu, A Chlipala, ...
arXiv preprint arXiv:2211.10665, 2022
15*2022
Omnisemantics: Smooth Handling of Nondeterminism
A Charguéraud, A Chlipala, A Erbsen, S Gruetter
ACM Transactions on Programming Languages and Systems 45 (1), 1-43, 2023
122023
Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises
A Erbsen, J Philipoom, J Gross, R Sloan, A Chlipala
2019 IEEE Symposium on Security and Privacy (SP) 1, 1202-1219, 2019
11*2019
Reification by parametricity: Fast setup for proof by reflection, in two lines of Ltac
J Gross, A Erbsen, A Chlipala
Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as …, 2018
102018
Crafting certified elliptic curve cryptography implementations in Coq
A Erbsen
Massachusetts Institute of Technology, 2017
102017
Integration Verification Across Software and Hardware for a Simple Embedded System. PLDI’21 (2021)
A Erbsen, S Gruetter, J Choi, C Wood, A Chlipala
82021
Foundational Integration Verification of a Cryptographic Server
A Erbsen, J Philipoom, D Jamner, A Lin, S Gruetter, C Pit-Claudel, ...
Proceedings of the ACM on Programming Languages 8 (PLDI), 1704-1729, 2024
52024
Accelerating Verified-Compiler Development with a Verified Rewriting Engine
J Gross, A Erbsen, J Philipoom, M Poddar-Agrawal, A Chlipala
arXiv preprint arXiv:2205.00862, 2022
52022
Certifying derivation of state machines from coroutines
M Ikebuchi, A Erbsen, A Chlipala
49th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages …, 2022
52022
Foundational Integration Verification of Diverse Software and Hardware Components
A Erbsen
Massachusetts Institute of Technology, 2023
32023
Distributed Authorization in Vanadium
A Erbsen, A Shankar, A Taly
arXiv preprint arXiv:1607.02192, 2016
32016
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq
J Gross, A Erbsen, J Philipoom, R Agrawal, A Chlipala
arXiv preprint arXiv:2305.02521, 2023
2023
Modeling High-Level Public-Key Cryptography in Coq
A Erbsen
2015
A Cryptographically Protected Phone System
A Erbsen, A Yedidia
2014
CryptOpt: Automatic Optimization of Straightline Code
J Kuepper, D Wu, A Erbsen, J Gross, O Conoly, C Sun, S Tian, A Chlipala, ...
The system can't perform the operation now. Try again later.
Articles 1–19