The ProVal team was stopped at the end of August 2012, and reborn into a new team
Toccata
These pages do not evolve anymore, please follow the link above for uptodate informations about our team.
Publications : Sylvie Boldo
Back[31]  Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Improving Real Analysis in Coq: a UserFriendly Approach to Integrals and Derivatives. In Proceedings of the The Second International Conference on Certified Programs and Proofs, Kyoto, Japan, December 2012. [ bib  full paper on HAL ] 
[30]  Sylvie Boldo, François Clément, JeanChristophe 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, 2012. Accepted for publication. http://hal.inria.fr/hal00649240/en/. [ bib  full paper on HAL ] 
[29] 
Sylvie Boldo, François Clément, JeanChristophe Filliâtre, Micaela
Mayero, Guillaume Melquiond, and Pierre Weis.
Wave equation numerical resolution: Mathematics and program.
Research Report 7826, INRIA, December 2011.
http://hal.inria.fr/hal00649240/en/.
[ bib 
full paper on HAL 
.pdf ]
We formally prove the C program that implements a simple numerical scheme for the resolution of the onedimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and the floatingpoint computation leads to roundoff errors. We formally specify in Coq the numerical scheme, prove both the method error and the roundoff error of the program, and derive an upper bound for the total error. This proves the adequacy of the C program to the numerical scheme and the convergence of the effective computation. To our knowledge, this is the first time a numerical analysis program is fully machinechecked. Keywords: Formal proof of numerical program; Convergence of numerical scheme; Proof of C program; Coq formal proof; Acoustic wave equation; Partial differential equation; Rounding error analysis 
[28]  Sylvie Boldo and Thierry Viéville. Représentation numérique de l'information. In Gilles Dowek, editor, Introduction à la science informatique, Repères pour agir, pages 2372. CRDP Académie de Paris, July 2011. [ bib  http ] 
[27]  Sylvie Boldo and Thierry Viéville. Structuration et contrôle de l'information. In Gilles Dowek, editor, Introduction à la science informatique, Repères pour agir, pages 281308. CRDP Académie de Paris, July 2011. [ bib  http ] 
[26] 
Sylvie Boldo and JeanMichel Muller.
Exact and Approximated error of the FMA.
IEEE Transactions on Computers, 60(2):157164, February 2011.
[ bib 
full paper on HAL ]
The fused multiply accumulateadd (FMA) instruction, specified by the IEEE 7542008 Standard for FloatingPoint Arithmetic, eases some calculations, and is already available on some current processors such as the Power PC or the Itanium. We first extend an earlier work on the computation of the exact error of an FMA (by giving more general conditions and providing a formal proof). Then, we present a new algorithm that computes an approximation to the error of an FMA, and provide error bounds and a formal proof for that algorithm.

[25]  Sylvie Boldo and Thi Minh Tuyen Nguyen. Proofs of numerical programs when the compiler optimizes. Innovations in Systems and Software Engineering, 7:151160, 2011. [ bib ] 
[24]  Sylvie Boldo and Claude Marché. Formal verification of numerical programs: from C annotated programs to mechanical proofs. Mathematics in Computer Science, 5:377393, 2011. [ bib  DOI  .pdf ] 
[23]  Sylvie Boldo and Guillaume Melquiond. Flocq: A unified library for proving floatingpoint algorithms in Coq. In Elisardo Antelo, David Hough, and Paolo Ienne, editors, Proceedings of the 20th IEEE Symposium on Computer Arithmetic, pages 243252, Tübingen, Germany, 2011. [ bib  .pdf ] 
[22]  Sylvie Boldo, François Clément, JeanChristophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Formal Proof of a Wave Equation Resolution Scheme: the Method Error. In Matt Kaufmann and Lawrence C. Paulson, editors, Proceedings of the first Interactive Theorem Proving Conference, volume 6172 of LNCS, pages 147162, Edinburgh, Scotland, July 2010. Springer. (merge of TPHOLs and ACL2). [ bib  full paper on HAL ] 
[21]  Sylvie Boldo. Formal verification of numerical programs: from C annotated programs to Coq proofs. In Proceedings of the Third International Workshop on Numerical Software Verification, Edinburgh, Scotland, July 2010. NSV8. [ bib  full paper on HAL ] 
[20]  Sylvie Boldo. Un algorithme de découpe de gâteau. Interstices, July 2010. http://interstices.info/decoupe. [ bib  http ] 
[19]  Sylvie Boldo and Thi Minh Tuyen Nguyen. Hardwareindependent proofs of numerical programs. In César Muñoz, editor, Proceedings of the Second NASA Formal Methods Symposium, NASA Conference Publication, pages 1423, Washington D.C., USA, April 2010. [ bib  full paper on HAL  PDF ] 
[18]  Sylvie Boldo. L'informatique. Universcience web television, April 2010. Quiz 512, http://www.universcience.tv/media/1340/linformatique.html. [ bib  full paper on HAL ] 
[17]  Sylvie Boldo. C'est la faute à l'ordinateur! Interstices  Idée reçue, February 2010. http://interstices.info/ideerecueinformatique18. [ bib  full paper on HAL ] 
[16]  Sylvie Boldo, JeanChristophe Filliâtre, and Guillaume Melquiond. Combining Coq and Gappa for Certifying FloatingPoint Programs. In 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, volume 5625 of Lecture Notes in Artificial Intelligence, pages 5974, Grand Bend, Canada, July 2009. Springer. [ bib ] 
[15]  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 91102, Rhodos, Greece, July 2009. Springer. [ bib ] 
[14]  Siegfried M. Rump, Paul Zimmermann, Sylvie Boldo, and Guillaume Melquiond. Computing predecessor and successor in rounding to nearest. BIT, 49(2):419431, June 2009. [ bib  full paper on HAL  PDF ] 
[13]  Sylvie Boldo. Kahan's algorithm for a correct discriminant computation at last formally proven. IEEE Transactions on Computers, 58(2):220225, February 2009. [ bib  DOI  full paper on HAL  PDF ] 
[12]  Sylvie Boldo. Demandez le programme! Interstices, February 2009. http://interstices.info/demandezleprogramme. [ bib  http ] 
[11]  Sylvie Boldo, Marc Daumas, and RenCang Li. Formally verified argument reduction with a fusedmultiplyadd. IEEE Transactions on Computers, 58(8):11391145, 2009. [ bib  DOI  PDF  http ] 
[10]  Sylvie Boldo. Demandez le programme! In DocSciences, volume 5, pages 2633. C.R.D.P. de l'académie de Versailles, November 2008. http://www.docsciences.fr/DocSciencesno5. [ bib  http ] 
[9]  Sylvie Boldo and Thierry Viéville. L'informatique, ce n'est pas pour les filles. Interstices, September 2008. http://interstices.info/ideerecueinformatique5. [ bib  http ] 
[8]  Sylvie Boldo, Marc Daumas, and Pascal Giorgi. Formal proof for delayed finite field arithmetic using floating point operators. In Marc Daumas and Javier Bruguera, editors, Proceedings of the 8th Conference on Real Numbers and Computers, pages 113122, Santiago de Compostela, Spain, July 2008. [ bib  full paper on HAL  PDF ] 
[7]  Sylvie Boldo. Pourquoi mon ordinateur calculetil faux? Interstices, April 2008. Podcast, http://interstices.info/aproposcalculordinateurs. [ bib  http ] 
[6]  Sylvie Boldo and Guillaume Melquiond. Emulation of FMA and CorrectlyRounded Sums: Proved Algorithms Using Rounding to Odd. IEEE Transactions on Computers, 57(4):462471, 2008. [ bib  full paper on HAL  PDF ] 
[5] 
Sylvie Boldo and JeanChristophe Filliâtre.
Formal Verification of FloatingPoint Programs.
In 18th IEEE International Symposium on Computer Arithmetic,
pages 187194, Montpellier, France, June 2007.
[ bib 
PDF 
.pdf ]
This paper introduces a methodology to perform formal verification of floatingpoint C programs. It extends an existing tool for the verification of C programs, Caduceus, with new annotations specific to floatingpoint arithmetic. The Caduceus firstorder logic model for C programs is extended accordingly. Then verification conditions expressing the correctness of the programs are obtained in the usual way and can be discharged interactively with the Coq proof assistant, using an existing Coq formalization of floatingpoint arithmetic. This methodology is already implemented and has been successfully applied to several short floatingpoint programs, which are presented in this paper.

[4]  Sylvie Boldo. Pitfalls of a full floatingpoint proof: example on the formal proof of the Veltkamp/Dekker algorithms. In Ulrich Furbach and Natarajan Shankar, editors, Third International Joint Conference on Automated Reasoning, volume 4130 of Lecture Notes in Computer Science, pages 5266, Seattle, USA, August 2006. Springer. [ bib  PDF  .pdf ] 
[3]  Sylvie Boldo and César Muñoz. Provably faithful evaluation of polynomials. In Proceedings of the 21st Annual ACM Symposium on Applied Computing, volume 2, pages 13281332, Dijon, France, April 2006. [ bib  full paper on HAL ] 
[2]  Sylvie Boldo, Marc Daumas, William Kahan, and Guillaume Melquiond. Proof and certification for an accurate discriminant. In 12th IMACSGAMM International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Duisburg,Germany, sep 2006. [ bib  http ] 
[1]  Sylvie Boldo and JeanMichel Muller. Some functions computable with a fusedmac. In Paolo Montuschi and Eric Schwarz, editors, Proceedings of the 17th Symposium on Computer Arithmetic, pages 5258, Cape Cod, USA, 2005. [ bib  .pdf ] 
Back
This page was generated by bibtex2html.