Research interests

  • Floating-point arithmetic.
  • Formal methods and proof assistants like Coq.
  • Formal verification of programs and numerical programs.

More information in my habilitation defended on October 6th, 2014.


  • vice-leader of the Toccata Inria project-team.
  • editorial committee of the popular science web site Interstices (French).
  • editorial board of Binaire, the blog of the French Computer Science Society (French)
  • head of the Coquelicot project (new Coq library for reals).
  • PC member of ARITH-22 (22nd IEEE Symposium on Computer Arithmetic) in June 2015.
  • PC member of the 7th Coq workshop in June 2015.
  • PC member of JFLA 2015 (26th "Journées Francophones des Langages Applicatifs") in January 2015.
  • PC member of the NSV 2014 (7th International Workshop on Numerical Software Verification) in July 2014.
  • head of the ended FOST project (Formal prOofs about Scientific compuTations).

Who am I?

I am an Inria researcher (Chargée 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).

Je suis très impliquée en médiation scientifique: voilà une liste de mes documents, exposés et activités. / I am into science popularization. Here is a list of my documents, talks and activities in French.

Recent selected publications

[BLM15 Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Coquelicot: A User-Friendly Library of Real Analysis for Coq. Mathematics in Computer Science, 9(1):41-62, 2015. [ bib | DOI | http ]
[BJLM15 Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. Verified Compilation of Floating-Point Computations. Journal of Automated Reasoning, 54(2):135-163, February 2015. [ bib | http ]
[BCF13 Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program. Journal of Automated Reasoning, 50(4):423-456, April 2013. [ bib | DOI | http ]
[BolNgu11 Sylvie Boldo and Thi Minh Tuyen Nguyen. Proofs of numerical programs when the compiler optimizes. Innovations in Systems and Software Engineering, 7:151-160, March 2011. [ bib ]
[BolMul11 Sylvie Boldo and Jean-Michel Muller. Exact and Approximated error of the FMA. IEEE Transactions on Computers, 60(2):157-164, February 2011. [ bib | http ]


Revue web de médiation scientifique
French popularization web journal