Symbolic Transformation of Expressions in Modular Arithmetic. - Jérôme Boillot; Jérôme Feret (SAS, 2023)

Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution). - Raphaël Monat; Marco Milanese; Francesco Parolini; Jérôme Boillot; Abdelraouf Ouadjaout; Antoine Miné (TACAS (3), 2024)

Abstraction of memory block manipulations by symbolic loop folding. - Jérôme Boillot; Jérôme Feret (ESOP (1), 2025)