Book cover

Book is out!

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-Sud).




Formal proof
Program verification

More keywords

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

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

  • 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