Aymeric Fromherz

29 papers A* 3B 1Journal 18Unranked 6
YearRankTypeTitle / Venue / Authors
2025 — conf
CUTECat: Concolic Execution for Computational Law.
ESOP (2)
Pierre Goutagny, Aymeric Fromherz, Raphaël Monat
2025 — conf
Charon: An Analysis Framework for Rust.
CAV (4)
Son Ho, Guillaume Boisseau, Lucas Franceschino, Yoann Prak, Aymeric Fromherz, Jonathan Protzenko
2024 J jnl
CUTECat: Concolic Execution for Computational Law.
CoRR
Pierre Goutagny, Aymeric Fromherz, Raphaël Monat
2024 J jnl
Charon: An Analysis Framework for Rust.
CoRR
Son Ho, Guillaume Boisseau, Lucas Franceschino, Yoann Prak, Aymeric Fromherz, Jonathan Protzenko
2024 J jnl
Compiling C to Safe Rust, Formalized.
CoRR
Aymeric Fromherz, Jonathan Protzenko
2024 — conf
Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law.
ESOP (2)
Raphaël Monat, Aymeric Fromherz, Denis Merigoux
2024 J jnl
Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law.
CoRR
Raphaël Monat, Aymeric Fromherz, Denis Merigoux
2024 J jnl
Sound Borrow-Checking for Rust via Symbolic Semantics.
CoRR
Son Ho, Aymeric Fromherz, Jonathan Protzenko
2024 J jnl
Sound Borrow-Checking for Rust via Symbolic Semantics.
Proc. ACM Program. Lang.
Son Ho, Aymeric Fromherz, Jonathan Protzenko
2024 J jnl
StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator.
CoRR
Antonin Reitz, Aymeric Fromherz, Jonathan Protzenko
2024 J jnl
StarMalloc: Verifying a Modern, Hardened Memory Allocator.
Proc. ACM Program. Lang.
Antonin Reitz, Aymeric Fromherz, Jonathan Protzenko
2023 B conf
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores.
CPP
Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, Ravi Ramamurthy
2023 J jnl
Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification.
Proc. ACM Program. Lang.
Son Ho, Aymeric Fromherz, Jonathan Protzenko
2022 — —
A Proof-Oriented Approach to Low-Level, High-Assurance Programming.
Aymeric Fromherz
2022 — conf
Self-correcting Neural Networks for Safe Classification.
NSV/FoMLAS@CAV
Klas Leino, Aymeric Fromherz, Ravi Mangal, Matt Fredrikson, Bryan Parno, Corina S. Pasareanu
2021 A* conf
Fast Geometric Projections for Local Robustness Certification.
ICLR
Aymeric Fromherz, Klas Leino, Matt Fredrikson, Bryan Parno, Corina S. Pasareanu
2021 J jnl
Self-Repairing Neural Networks: Provable Safety for Deep Networks via Dynamic Repair.
CoRR
Klas Leino, Aymeric Fromherz, Ravi Mangal, Matt Fredrikson, Bryan Parno, Corina S. Pasareanu
2021 J jnl
Steel: proof-oriented programming in a dependently typed concurrent separation logic.
Proc. ACM Program. Lang.
Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Martínez, Denis Merigoux, Tahina Ramananandro
2021 J jnl
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs.
CoRR
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, Guido Martínez
2020 A* conf
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider.
SP
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
2020 J jnl
Fast Geometric Projections for Local Robustness Certification.
CoRR
Aymeric Fromherz, Klas Leino, Matt Fredrikson, Bryan Parno, Corina S. Pasareanu
2020 A* conf
HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms).
CCS
Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella-Béguelin
2020 J jnl
HACL×N: Verified Generic SIMD Crypto (for all your favorite platforms).
IACR Cryptol. ePrint Arch.
Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella-Béguelin
2020 J jnl
SteelCore: an extensible concurrent separation logic for effectful dependently typed programs.
Proc. ACM Program. Lang.
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, Guido Martínez
2019 J jnl
A verified, efficient embedding of a verifiable assembly language.
Proc. ACM Program. Lang.
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, Nikhil Swamy
2019 J jnl
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider.
IACR Cryptol. ePrint Arch.
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
2019 — conf
Symbolic Pathfinder for SV-COMP - (Competition Contribution).
TACAS (3)
Yannic Noller, Corina S. Pasareanu, Aymeric Fromherz, Xuan-Bach Dinh Le, Willem Visser
2018 — conf
Static Value Analysis of Python Programs by Abstract Interpretation.
NFM
Aymeric Fromherz, Abdelraouf Ouadjaout, Antoine Miné
2016 J jnl
Symbolic Arrays in Symbolic PathFinder.
ACM SIGSOFT Softw. Eng. Notes
Aymeric Fromherz, Kasper Søe Luckow, Corina S. Pasareanu