Andres Erbsen

Orcid: 0000-0002-9854-7500

According to our database1, Andres Erbsen authored at least 14 papers between 2018 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

On csauthors.net:

Bibliography

2024
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq.
J. Autom. Reason., September, 2024

Foundational Integration Verification of a Cryptographic Server.
Proc. ACM Program. Lang., 2024

2023
Flexible Instruction-Set Semantics via Abstract Monads (Experience Report).
Proc. ACM Program. Lang., August, 2023

Omnisemantics: Smooth Handling of Nondeterminism.
ACM Trans. Program. Lang. Syst., March, 2023

CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives.
Proc. ACM Program. Lang., 2023

CryptOpt: Automatic Optimization of Straightline Code.
Proceedings of the 45th IEEE/ACM International Conference on Software Engineering: ICSE 2023 Companion Proceedings, 2023

2022
Certifying derivation of state machines from coroutines.
Proc. ACM Program. Lang., 2022

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

Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code.
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.
Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

2021
A Multipurpose Formal RISC-V Specification.
CoRR, 2021

Integration verification across software and hardware for a simple embedded system.
Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

2020
Simple High-Level Code For Cryptographic Arithmetic: With Proofs, Without Compromises.
ACM SIGOPS Oper. Syst. Rev., 2020

2018
Reification by Parametricity - Fast Setup for Proof by Reflection, in Two Lines of Ltac.
Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018


  Loading...