- 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?
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 ]|