Research interests
- Floating-point arithmetic.
- Formal methods and proof assistants like Coq.
- Formal verification of programs and numerical programs.
Responsabilities
- editorial committee of the popular science web site Interstices (in French only).
- head of the FOST project (Formal prOofs about Scientific compuTations).
Who am I?
I am an INRIA researcher (Chargée de recherche) in Orsay, France, in the Proval project.
I work at the INRIA Saclay - Île-de-France research unit and in the Laboratoire de Recherche en Informatique (Université Paris Sud).
Recent selected publications
| [BCF10] | Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Formal Proof of a Wave Equation Resolution Scheme: the Method Error. In Proceedings of the first Interactive Theorem Proving Conference, LNCS, Edinburgh, Scotland, July 2010. Springer. [ bib | http ] |
| [BolNgu10] | Sylvie Boldo and Thi Minh Tuyen Nguyen. Hardware-independent proofs of numerical programs. In Proceedings of the Second NASA Formal Methods Symposium, NASA Conference Publication, Washington D.C., USA, April 2010. [ bib ] |
| [BolMul10] | Sylvie Boldo and Jean-Michel Muller. Exact and Approximated error of the FMA. IEEE Transactions on Computers, 2010. Minor revision. [ bib | http ] |
| [Bol09b] | Sylvie Boldo. Floats & Ropes: a case study for formal numerical program verification. In 36th International Colloquium on Automata, Languages and Programming, volume 5556 of Lecture Notes in Computer Science - ARCoSS, pages 91-102, Rhodos, Greece, July 2009. Springer. [ bib | DOI | .pdf ] |
| [Bol09a] | Sylvie Boldo. Kahan's algorithm for a correct discriminant computation at last formally proven. IEEE Transactions on Computers, 58(2):220-225, February 2009. [ bib | DOI | http ] |