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).
- elected member of the Inria Evaluation Committee.
- head of the FOST project (Formal prOofs about Scientific compuTations).
- head of the Coquelicot project (new Coq library for reals).
- PC member of the JFLA 2011 (22e journées francophones des langages applicatifs)
- PC member of the NSV 2011 (4th International Workshop on Numerical Software Verification)
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).
Je suis très impliquée en médiation scientifique: voilà une liste de mes documents et exposés de vulgarisation scientifique. / I am into science popularization. Here is a list of my documents and talks in French.
Recent selected publications
|
Introduction à la science informatique Repères pour agir. CRDP Académie de Paris, July 2011, edited by Gilles Dowek, is now available at Amazon and Decitre. |
| [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 | .pdf ] |
| [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 ] |
