Publications

• StarMalloc: Verifying a Modern, Hardened Memory Allocator. Antonin Reitz, Aymeric Fromherz, Jonathan Protzenko, International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 2024.
• Sound Borrow-Checking for Rust via Symbolic Semantics. Son Ho, Aymeric Fromherz, Jonathan Protzenko, International Conference on Functional Programming (ICFP), 2024.
• Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law. Raphaël Monat, Aymeric Fromherz, Denis Merigoux. European Symposium on Programming (ESOP), 2024, Best Tool Paper Award.
• Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification. Son Ho, Aymeric Fromherz, Jonathan Protzenko. International Conference on Functional Programming (ICFP), 2023.
• FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores. Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, Ravi Ramamurthy. International Conference on Certified Programs and Proofs (CPP), 2023.
• Self-Correcting Neural Networks for Safe Classification, Klas Leino, Aymeric Fromherz, Ravi Mangal, Matt Fredrikson, Bryan Parno, Corina Păsăreanu. Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS), 2022
• Turning Catala into a Proof Platform for the Law. Alain Delaët, Denis Merigoux, Aymeric Fromherz. Programming Languages and the Law (ProLaLa), 2022.
• A Proof-Oriented Approach to Low-Level, High-Assurance Programming. Aymeric Fromherz. PhD thesis, 2021.
• Steel: Proof-Oriented Programming in a Dependently Typed Concurrent Separation Logic. Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Martinez, Denis Merigoux, Tahina Ramananandro. International Conference on Functional Programming (ICFP), 2021.
• Fast Geometric Projections for Local Robustness Certification. Aymeric Fromherz, Klas Leino, Matt Fredrikson, Bryan Parno, Corina S. Păsăreanu. International Conference on Learning Representations (ICLR), 2021, (Spotlight paper).
• HACL×N: Verified Generic SIMD Crypto (for all your favorite platforms). Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella-Béguelin. ACM Conference on Computer and Communication Security (CCS), 2020.
• SteelCore: an Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs. Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, Guido Martinez. Proceedings of the ACM International Conference on Functional Programming (ICFP), 2020.
• Steel: Scaling Up Memory Reasoning for F*. Denis Merigoux, Aymeric Fromherz. Automated Deduction for Separation Logics (ADSL), 2020.
• EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cedric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph Wintersteiger, Santiago Zanella-Beguelin. Proceedings of the IEEE Symposium on Security and Privacy (S&P), 2020.
• Symbolic Pathfinder for SV-COMP (Competition Contribution). Yannic Noller, Corina S. Păsăreanu, Aymeric Fromherz, Xuan-Bach D. Le, Willem Visser. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019). Lecture Notes in Computer Science, vol 11429. (Publisher version)
• A Verified, Efficient Embedding of a Verifiable Assembly Language. Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, Nikhil Swamy. Proceedings of the ACM Symposium on Principles of Programming Languages (POPL), January, 2019
• Static Value Analysis of Python Programs by Abstract Interpretation. Aymeric Fromherz, Abdelraouf Ouadjaout, Antoine Miné. In Proc. of 10th NASA Formal Methods Symposium (NFM'18), 185–202, Newport News, USA, Apr. 2018. Springer. (Publisher version)
• Symbolic Arrays in Symbolic PathFinder. Aymeric Fromherz, Kasper Søe Luckow, Corina S. Păsăreanu. SIGSOFT Softw. Eng. Notes, 2017, 41(6), 1–5. https://doi.org/10.1145/3011286.3011296

Preprints

• Charon: An Analysis Framework for Rust. Son Ho, Guillaume Boisseau, Lucas Franceschino, Yoann Prak, Aymeric Fromherz, Jonathan Protzenko
• CUTECat: Concolic Execution for Computational Law. Pierre Goutagny, Aymeric Fromherz, Raphaël Monat
• Compiling C to Safe Rust, FormalizedAymeric Fromherz, Jonathan Protzenko

Technical Reports

• Programming and Proving with Indexed Effects. Aseem Rastogi, Guido Martinez, Aymeric Fromherz, Tahina Ramananandro, Nikhil Swamy. Technical Report, 2021.