Symbolic Arrays in Symbolic PathFinder. - Aymeric Fromherz; Kasper Søe Luckow; Corina S. Pasareanu (ACM SIGSOFT Softw. Eng. Notes, 2016)

Static Value Analysis of Python Programs by Abstract Interpretation. - Aymeric Fromherz; Abdelraouf Ouadjaout; Antoine Miné (NFM, 2018)

Symbolic Pathfinder for SV-COMP - (Competition Contribution). - Yannic Noller; Corina S. Pasareanu; Aymeric Fromherz; Xuan-Bach Dinh Le 001; Willem Visser (TACAS (3), 2019)

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; Cédric Fournet; Tahina Ramananandro; Aseem Rastogi; et al. (IACR Cryptol. ePrint Arch., 2019)

A verified, efficient embedding of a verifiable assembly language. - Aymeric Fromherz; Nick Giannarakis; Chris Hawblitzel; Bryan Parno; Aseem Rastogi; Nikhil Swamy (Proc. ACM Program. Lang., 2019)

HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms). - Marina Polubelova; Karthikeyan Bhargavan; Jonathan Protzenko; Benjamin Beurdouche; Aymeric Fromherz; Natalia Kulatova; Santiago Zanella-Béguelin (CCS, 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; Cédric Fournet; Natalia Kulatova; Tahina Ramananandro; et al. (SP, 2020)

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 (IACR Cryptol. ePrint Arch., 2020)

SteelCore: an extensible concurrent separation logic for effectful dependently typed programs. - Nikhil Swamy; Aseem Rastogi; Aymeric Fromherz; Denis Merigoux; Danel Ahman; Guido Martínez (Proc. ACM Program. Lang., 2020)

Fast Geometric Projections for Local Robustness Certification. - Aymeric Fromherz; Klas Leino; Matt Fredrikson; Bryan Parno; Corina S. Pasareanu (ICLR, 2021)

Self-Repairing Neural Networks: Provable Safety for Deep Networks via Dynamic Repair. - Klas Leino; Aymeric Fromherz; Ravi Mangal; Matt Fredrikson; Bryan Parno; Corina S. Pasareanu (CoRR, 2021)

Steel: proof-oriented programming in a dependently typed concurrent separation logic. - Aymeric Fromherz; Aseem Rastogi; Nikhil Swamy; Sydney Gibson; Guido Martínez; Denis Merigoux; Tahina Ramananandro (Proc. ACM Program. Lang., 2021)

Self-correcting Neural Networks for Safe Classification. - Klas Leino; Aymeric Fromherz; Ravi Mangal; Matt Fredrikson; Bryan Parno; Corina S. Pasareanu (NSV/FoMLAS@CAV, 2022)

A Proof-Oriented Approach to Low-Level, High-Assurance Programming. - Aymeric Fromherz (2022)

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 (CPP, 2023)

Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification. - Son Ho; Aymeric Fromherz; Jonathan Protzenko (Proc. ACM Program. Lang., 2023)

Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law. - Raphaël Monat; Aymeric Fromherz; Denis Merigoux (ESOP (2), 2024)

StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator. - Antonin Reitz; Aymeric Fromherz; Jonathan Protzenko (CoRR, 2024)

Compiling C to Safe Rust, Formalized. - Aymeric Fromherz; Jonathan Protzenko (CoRR, 2024)

Sound Borrow-Checking for Rust via Symbolic Semantics. - Son Ho; Aymeric Fromherz; Jonathan Protzenko (Proc. ACM Program. Lang., 2024)

StarMalloc: Verifying a Modern, Hardened Memory Allocator. - Antonin Reitz; Aymeric Fromherz; Jonathan Protzenko (Proc. ACM Program. Lang., 2024)

Charon: An Analysis Framework for Rust. - Son Ho; Guillaume Boisseau; Lucas Franceschino; Yoann Prak; Aymeric Fromherz; Jonathan Protzenko (CAV (4), 2025)

CUTECat: Concolic Execution for Computational Law. - Pierre Goutagny; Aymeric Fromherz; Raphaël Monat (ESOP (2), 2025)