Sylvie Boldo

Sylvie Boldo is a French mathematician and computer scientist. Her research combines automated theorem proving and computer arithmetic, focusing on the formal verification of floating-point arithmetic operations and of algorithms based on them. She is a director of research for the French Institute for Research in Computer Science and Automation (INRIA), affiliated with the Formal Methods Laboratory at Paris-Saclay University and the INRIA Saclay-Île-de-France Research Centre, where she co-leads the Toccata project for formally verified programs, certified tools and numerical computations. She is also the founding jury president for the French agrégation in computer science.

Education and career Boldo completed her Ph.D. at the École normale supérieure de Lyon in 2004, and has been affiliated with INRIA Saclay since 2005. She completed her habilitation at Paris-Sud University in 2014, with the habilitation thesis Deductive Formal Verification: How To Make Your Floating-Point Programs Behave.

In 2021, France began offering an agrégation in computer science, and selected Boldo as the founding president of its jury.

Books Boldo is the author of books including: Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System (with Guillaume Melquiond, ISTE Press / Elsevier, 2017) Une introduction à la science informatique pour les enseignants de la discipline en lycée (with Dowek, Archambault, Baccelli, Bouhinou, Cegielski, Clausen, Guessarian, Lopes, Mounier, Nguyen, Quessette, Rasse, Rozoy, Timsit, Viéville, and Vincent, CRDP Paris, 2011)