On the way to certify Computer Algebra Systems. - Sylvain Boulmé; Thérèse Hardin; Daniel Hirschkoff; Valérie Ménissier-Morain; Renaud Rioboo (Calculemus, 1999)

Certifying Synchrony for Free. - Sylvain Boulmé; Grégoire Hamon (LPAR, 2001)

Adaptable Translator of B Specifications to Embedded C Programs. - Didier Bert; Sylvain Boulmé; Marie-Laure Potet; Antoine Requet; Laurent Voisin (FME, 2003)

Adaptabilité et validation de la traduction de B vers C. Points de vue et résultats du projet BOM. - Frédéric Badeau; Didier Bert; Sylvain Boulmé; Christophe Métayer; Marie-Laure Potet; Nicolas Stouls; Laurent Voisin (Tech. Sci. Informatiques, 2004)

Proof Contexts with Late Binding. - Virgile Prevosto; Sylvain Boulmé (TLCA, 2005)

Interpreting Invariant Composition in the B Method Using the Spec# Ownership Relation: A Way to Explain and Relax B Restrictions. - Sylvain Boulmé; Marie-Laure Potet (B, 2007)

Intuitionistic Refinement Calculus. - Sylvain Boulmé (TLCA, 2007)

Relaxing Restrictions on Invariant Composition in the B Method by Ownership Control a laSpec#. - Sylvain Boulmé; Marie-Laure Potet (Rigorous Methods for Software Construction and Analysis, 2009)

A Refinement Methodology for Object-Oriented Programs. - Asma Tafat; Sylvain Boulmé; Claude Marché (FoVeOOS, 2010)

A Certifying Frontend for (Sub)polyhedral Abstract Domains. - Alexis Fouilhé; Sylvain Boulmé (VSTTE, 2014)

A Coq Tactic for Equality Learning in Linear Arithmetic. - Sylvain Boulmé; Alexandre Maréchal (ITP, 2018)

The Verified Polyhedron Library: an Overview. - Sylvain Boulmé; Alexandre Maréchal; David Monniaux; Michaël Périn; Hang Yu 005 (SYNASC, 2018)

Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra. - Sylvain Boulmé; Alexandre Maréchal (J. Autom. Reason., 2019)

Certified and efficient instruction scheduling: application to interlocked VLIW processors. - Cyril Six; Sylvain Boulmé; David Monniaux (Proc. ACM Program. Lang., 2020)

Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles). (Programmation défensive formellement vérifiée (calculs efficaces et vérifiés en Coq, à partir d'oracles OCaml potentiellement non fiables)). - Sylvain Boulmé (2021)

Formally verified superblock scheduling. - Cyril Six; Léo Gourdin; Sylvain Boulmé; David Monniaux; Justus Fasse; Nicolas Nardino (CPP, 2022)

The Trusted Computing Base of the CompCert Verified Compiler. - David Monniaux; Sylvain Boulmé (ESOP, 2022)

Testing a Formally Verified Compiler. - David Monniaux; Léo Gourdin; Sylvain Boulmé; Olivier Lebeltel (TAP, 2023)

Formally Verifying Optimizations with Block Simulations. - Léo Gourdin; Benjamin Bonneau; Sylvain Boulmé; David Monniaux; Alexandre Bérard (Proc. ACM Program. Lang., 2023)

Formally Verified Hardening of C Programs against Hardware Fault Injection. - Basile Pesin; Sylvain Boulmé; David Monniaux; Marie-Laure Potet (CPP, 2025)