• [Jun 20] Accepted paper at IEEE Transactions on Computers, with C. Lauter and J.-M. Muller about the emulation of round-to-nearest ties-to-zero
  • [Jun 20] The ARITH-2020 face-to-face meeting of Jun 7-10, 2020 in Portland, Oregon has been cancelled
  • [Apr 20] Accepted paper at ARITH-2020: A Correctly-Rounded Fixed-Point-Arithmetic Dot-Product Algorithm, with Diane Gallois-Wong and Thibault Hilaire
  • [March 20] I belong to the crisis unit of Inria Saclay
  • [Jan 20] Invited speaker at Formal Methods in Mathematics / Lean Together 2020 at Carnegie Mellon University
  • [Dec 19] Invited at Collège de France by Xavier Leroy Video here
  • [Dec 20] My PhD student Florian Faissole got his PhD
  • [Dec 20] 3 PhDs in one week: president of the PhD defense of Yohan Chatelain, Université Paris-Saclay; president of the PhD defense of Armaël Guéneau, Université de Paris; member of the PhD defense of Antoine Kaszczyc, Université Paris-Nord
Book cover


At the end of 2017, Guillaume Melquiond and I published a book that provides a comprehensive view of how to formally specify and verify tricky floating-point algorithms with the Coq proof assistant. It describes the Flocq formalization of floating-point arithmetic and some methods to automate theorem proofs. It then presents the specification and verification of various algorithms, from error-free transformations to a numerical scheme for a partial differential equation. The examples cover not only mathematical algorithms but also C programs as well as issues related to compilation. Buy it here or here.

Photo of S. Boldo

Who am I?

I am an Inria research director (Directrice de recherche) in Orsay, France, in the Toccata project.

I work at the Inria Saclay - Île-de-France research unit and in the VALS team of the Laboratoire de Recherche en Informatique (CNRS and Université Paris-Saclay).



Formalization of mathematics

Formal proof
Program verification

More keywords

I created a word cloud using wordclouds from the titles of my publication: word cloud - female shape


I translated as best as I could. I let the French version when useful.
  • Deputy Scientific Head of Inria Saclay (Déléguée Scientifique Adjointe, DSA)
  • member of the Scientific Council of CentraleSupélec
  • elected chair of the ARITH working group of the GDR-IM (a CNRS subgroup of computer science)
  • member of the (temporary) council of the Computer Science Graduate School of Université Paris-Saclay
  • member of the CoDiReV Paris-Saclay (committee of the research heads of the Paris-Saclay components and partners)
  • deputy member of the CFVU Paris-Saclay (commission de la formation et de la vie universitaire)
  • member of the CDT commission of Inria Saclay (commission de développement technologique) for selecting engineering positions
  • member of the partners commission for the Digicosme Labex (comité des tutelles du labex Digicosme)
  • member of the program committee for selecting postdocs of the maths/computer science program of the Labex mathématique Hadamard
  • member of the (national) Inria IES commission (commission pour l'information et l'édition scientifique) about scientific edition and publication models
  • member of the Inria Saclay CLFP (commission locale de formation permanente)
I used to be (see also my popularization page):
  • member of the STIC department commission of Université Paris-Sud (2019-2020)
  • member of the executive commission for the Digicosme Labex (comité exécutif du labex Digicosme) (2019-2020)
  • member of the committee for the Gilles Kahn PhD award of the French Computer Science Society (2015-2017)
  • member of the Inria evaluation committee (2011-2014)

Program Committees

PhD students


I got the Best Talk Award at the Numerical Sotware Verification 2016 conference for my talk about Computing a correct and tight rounding error bound using rounding-to-nearest.

Funded projects

  • EMC2, ERC Synergy project about Extreme-scale Mathematically-based Computational Chemistry, 2019-2025, member
  • MILC, DIM-RFSI project about Lebesgue integration in Coq, 2018-2020, member
  • ELEFFAN, DigiCosme project, rounding errors of numerical schemes, 2016-2019, PI
  • ELFIC DigiCosme working group, certification about the finite element method, 2014-2016, PI
  • FastRelax ANR project, fast and reliable approximation algorithms, 2014-2018, site leader
  • Coquelicot Digiteo project, new Coq library for reals, 2011-2014, PI
  • Verasco ANR project, verified static analyzers and compilers, 2011-2015
  • FOST ANR project, formal proofs about scientific computations, 2009-2012, PI
  • HISSEO Digiteo project, handling compiler discrepancies when verifying floating-point programs, 2008-2012
  • CERPAN ANR project, certification of applied mathematics programs, 2005-2008, site leader