Wiki Agenda Contact Version française

Publications : Sylvie Boldo

Back
[53] Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, and Valentina Popescu. Formal verification of a floating-point expansion renormalization algorithm. In Proceedings of the 8th International Conference on Interactive Theorem Proving, Brasilia, Brazil, September 2017. [ bib | full text on HAL | .pdf ]
[52] Sylvie Boldo, Florian Faissole, and Alexandre Chapoutot. Round-off error analysis of explicit one-step numerical integration methods. In 24th IEEE Symposium on Computer Arithmetic, London, United Kingdom, July 2017. [ bib | DOI | full text on HAL | .pdf ]
[51] Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. Preuve formelle du théorème de Lax--Milgram. In 16èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels, Montpellier, France, June 2017. [ bib | full text on HAL | .pdf ]
[50] Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq Formal Proof of the Lax-Milgram theorem. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 79--89, New York, NY, USA, January 2017. ACM. [ bib | DOI | full text on HAL | .pdf ]
[49] Sylvie Boldo. Computing a correct and tight rounding error bound using rounding-to-nearest. In 9th International Workshop on Numerical Software Verification, Toronto, Canada, July 2016. [ bib | full text on HAL | .pdf ]
[48] Sylvie Boldo. Iterators: where folds fail. In Workshop on High-Consequence Control Verification, Toronto, Canada, July 2016. [ bib | full text on HAL | .pdf ]
[47] Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Formalization of real analysis: A survey of proof assistants and libraries. Mathematical Structures in Computer Science, 2016. [ bib | full text on HAL ]
[46] Sylvie Boldo. Formal Verification of Programs Computing the Floating-Point Average. In Michael Butler, Sylvain Conchon, and Fatiha Zaïdi, editors, 17th International Conference on Formal Engineering Methods, volume 9407 of Lecture Notes in Computer Science, pages 17--32, Paris, France, November 2015. Springer. [ bib | full text on HAL | .pdf ]
[45] 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, June 2015. [ bib | DOI | full text on HAL ]
[44] Sylvie Boldo. Stupid is as stupid does: Taking the square root of the square of a floating-point number. In Sergiy Bogomolov and Matthieu Martel, editors, Proceedings of the Seventh and Eighth International Workshop on Numerical Software Verification, volume 317 of Electronic Notes in Theoretical Computer Science, pages 50--55, Seattle, WA, USA, April 2015. [ bib | DOI | full text on HAL ]
[43] Thierry Vieville, Sylvie Boldo, Florent Masseglia, and Pierre Bernhard. Structures : organisation, complexité, dynamique des mot-clés au sens inattendu, April 2015. Article de vulgarisation sur pixees.fr. [ bib | full text on HAL ]
[42] 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 | full text on HAL ]
[41] Sylvie Boldo and Jean-Michel Muller. Des ordinateurs capables de calculer plus juste. La Recherche, 492:46--52, October 2014. [ bib | full text on HAL ]
[40] Sylvie Boldo. Même les ordinateurs font des erreurs ! In Martin Andler, Liliane Bel, Sylvie Benzoni-Gavage, Thierry Goudon, Cyril Imbert, and Antoine Rousseau, editors, Brèves de maths, pages 136--137. Nouveau Monde Editions, October 2014. [ bib | full text on HAL | http ]
[39] Sylvie Boldo. Deductive Formal Verification: How To Make Your Floating-Point Programs Behave. Thèse d'habilitation, Université Paris-Sud, October 2014. [ bib | full text on HAL ]
[38] Sylvie Boldo. Formal verification of tricky numerical computations. In 16th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Würzburg, Germany, September 2014. Invited talk. [ bib | full text on HAL | http ]
[37] Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program. Computers and Mathematics with Applications, 68(3):325--352, 2014. [ bib | DOI | full text on HAL | http ]
[36] 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 | full text on HAL ]
[35] Antoine Rousseau, Aurélie Darnaud, Brice Goglin, Céline Acharian, Christine Leininger, Christophe Godin, Clarisse Holik, Claude Kirchner, Diane Rives, Elodie Darquie, Erwan Kerrien, Fabrice Neyret, Florent Masseglia, Florian Dufour, Gérard Berry, Gilles Dowek, Hélène Robak, Hélène Xypas, Irina Illina, Isabelle Gnaedig, Joanna Jongwane, Jocelyne Ehrel, Laurent Viennot, Laure Guion, Lisette Calderan, Lola Kovacic, Marie Collin, Marie-Agnès Enard, Marie-Hélène Comte, Martin Quinson, Martine Olivi, Mathieu Giraud, Mathilde Dorémus, Mia Ogouchi, Muriel Droin, Nathalie Lacaux, Nicolas Rougier, Nicolas Roussel, Pascal Guitton, Pierre Peterlongo, Rose-Marie Cornus, Simon Vandermeersch, Sophie Maheo, Sylvain Lefebvre, Sylvie Boldo, Thierry Viéville, Véronique Poirel, Aline Chabreuil, Arnaud Fischer, Claude Farge, Claude Vadel, Isabelle Astic, Jean-Pierre Dumont, Loic Féjoz, Patrick Rambert, Pierre Paradinas, Sophie De Quatrebarbes, and Stéphane Laurent. Médiation scientifique : une facette de nos métiers de la recherche. Interne, Inria, March 2013. [ bib | full text on HAL | http ]
Dans ce monde devenu numérique nous savons que c'est une de nos missions d'acteur de la recherche publique, que de rendre accessibles les sciences du numérique au plus grand nombre. Ceci afin que chaque citoyenne et citoyen maîtrise, au delà des usages, les principaux fondements de cette mutation numérique. Et nous croyons que c'est l'acquisition d'une culture scientifique sur ces sujets qui est le levier de cette appropriation. C'est notre mission et notre plaisir d'y contribuer. Ce document a pour but d'aider chaque collègue Inria intéressé à participer à ce volet de nos missions. Devenue une facette de notre métier, comme le rappelle le Plan Stratégique Inria [1], ce que nous appelons médiation scientifique en sciences du numérique (alias, " mecsci ") se professionnalise et change d'échelle. Et c'est environ 1 % de nos ressources qui a vocation à y être consacré. Pour tout l'institut on parle donc de près de 40 équivalents temps-plein distribués à travers le travail quotidien ou ponctuel de plusieurs centaines de collègues chercheurs, ingénieurs, communicants, etc.. Une telle énergie mérite d'être bien employée : au service des meilleurs objectifs ; vers des cibles bien définies qui ont de vrais besoins sur ces sujets ; dans le cadre d'actions leviers qui aident à faire bouger les choses ; et avec une méthodologie efficace qui optimise ce que nous investissons dans de telles activités ; tout en respectant et en encourageant les dynamiques locales et individuelles indépendantes qui restent les sources vives de la médiation scientifique. Voilà pourquoi il y a juste besoin d'offrir en partage à chacune et chacun les éléments fondateurs et méthodologiques de cette médiation scientifique. Offrir aussi quelques bonnes pratiques très concrètes. On parle donc ici d'une organisation distribuée d'actions collaboratives d'où émerge le service public de popularisation scientifique visé. C'est ce que ce document se propose de décrire ici.

Keywords: médiation scientifique ; culture scientifique ; recherche ; popularisation des sciences ; service public.
[34] Sylvie Boldo. How to compute the area of a triangle: a formal revisit. In Proceedings of the 21th IEEE Symposium on Computer Arithmetic, Austin, Texas, USA, 2013. [ bib | full text on HAL ]
[33] Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. A formally-verified C compiler supporting floating-point arithmetic. In Proceedings of the 21th IEEE Symposium on Computer Arithmetic, Austin, Texas, USA, 2013. [ bib | full text on HAL ]
[32] Sylvie Boldo and Guillaume Melquiond. Informatique Mathématique, une photographie en 2013, chapter Arithmétique des ordinateurs et preuves formelles, pages 189--220. Presses Universitaires de Perpignan, Perpignan, France, 2013. [ bib | full text on HAL ]
[31] Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Improving real analysis in Coq: a user-friendly approach to integrals and derivatives. In Chris Hawblitzel and Dale Miller, editors, Proceedings of the Second International Conference on Certified Programs and Proofs, volume 7679 of Lecture Notes in Computer Science, pages 289--304, Kyoto, Japan, December 2012. [ bib | DOI | full text on HAL ]
[30] Sylvie Boldo and Guillaume Melquiond. Arithmétique des ordinateurs et preuves formelles. In Valérie Berthé, Christiane Frougny, Natacha Portier, Marie-Françoise Roy, and Anne Siegel, editors, École des Jeunes Chercheurs en Informatique Mathématique, pages 1--30. Rennes, France, March 2012. [ bib | full text on HAL ]
[29] Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Wave equation numerical resolution: Mathematics and program. Research Report 7826, INRIA, December 2011. [ bib | full text on HAL ]
We formally prove the C program that implements a simple numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and the floating-point computation leads to round-off errors. We formally specify in Coq the numerical scheme, prove both the method error and the round-off 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 machine-checked.

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 23--72. 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 281--308. CRDP Académie de Paris, July 2011. [ bib | http ]
[26] Sylvie Boldo and Jean-Michel Muller. Exact and Approximated error of the FMA. IEEE Transactions on Computers, 60(2):157--164, February 2011. [ bib | full text on HAL ]
The fused multiply accumulate-add (FMA) instruction, specified by the IEEE 754-2008 Standard for Floating-Point 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:151--160, 2011. [ bib | full text on HAL ]
[24] Sylvie Boldo and Claude Marché. Formal verification of numerical programs: from C annotated programs to mechanical proofs. Mathematics in Computer Science, 5:377--393, 2011. [ bib | DOI | full text on HAL | .pdf ]
[23] Sylvie Boldo and Guillaume Melquiond. Flocq: A unified library for proving floating-point algorithms in Coq. In Elisardo Antelo, David Hough, and Paolo Ienne, editors, Proceedings of the 20th IEEE Symposium on Computer Arithmetic, pages 243--252, Tübingen, Germany, 2011. [ bib | DOI | full text on HAL ]
[22] 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 Matt Kaufmann and Lawrence C. Paulson, editors, Proceedings of the First Interactive Theorem Proving Conference, volume 6172 of LNCS, pages 147--162, Edinburgh, Scotland, July 2010. Springer. [ bib | DOI | full text 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. NSV-8. [ bib | full text 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. Hardware-independent proofs of numerical programs. In César Muñoz, editor, Proceedings of the Second NASA Formal Methods Symposium, NASA Conference Publication, pages 14--23, Washington D.C., USA, April 2010. [ bib | full text on HAL | PDF ]
[18] Sylvie Boldo. L'informatique. Universcience web television, April 2010. Quiz 5-12, http://www.universcience.tv/media/1340/l-informatique.html. [ bib | full text on HAL ]
[17] Sylvie Boldo. C'est la faute à l'ordinateur! Interstices -- Idée reçue, February 2010. http://interstices.info/idee-recue-informatique-18. [ bib | full text on HAL ]
[16] Sylvie Boldo, Jean-Christophe Filliâtre, and Guillaume Melquiond. Combining Coq and Gappa for Certifying Floating-Point Programs. In 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, volume 5625 of Lecture Notes in Artificial Intelligence, pages 59--74, Grand Bend, Canada, July 2009. Springer. [ bib | DOI ]
[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 91--102, 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):419--431, June 2009. [ bib | DOI | full text on HAL ]
[13] 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 | full text on HAL | PDF ]
[12] Sylvie Boldo. Demandez le programme! Interstices, February 2009. http://interstices.info/demandez-le-programme. [ bib | http ]
[11] Sylvie Boldo, Marc Daumas, and Ren-Cang Li. Formally verified argument reduction with a fused-multiply-add. IEEE Transactions on Computers, 58(8):1139--1145, 2009. [ bib | DOI | PDF | http ]
[10] Sylvie Boldo. Demandez le programme! In DocSciences, volume 5, pages 26--33. C.R.D.P. de l'académie de Versailles, November 2008. http://www.docsciences.fr/-DocSciences-no5-. [ bib | http ]
[9] Sylvie Boldo and Thierry Viéville. L'informatique, ce n'est pas pour les filles. Interstices, September 2008. http://interstices.info/idee-recue-informatique-5. [ 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 113--122, Santiago de Compostela, Spain, July 2008. [ bib | full text on HAL | PDF ]
[7] Sylvie Boldo. Pourquoi mon ordinateur calcule-t-il faux? Interstices, April 2008. Podcast, http://interstices.info/a-propos-calcul-ordinateurs. [ bib | http ]
[6] Sylvie Boldo and Guillaume Melquiond. Emulation of FMA and Correctly-Rounded Sums: Proved Algorithms Using Rounding to Odd. IEEE Transactions on Computers, 57(4):462--471, 2008. [ bib | DOI | full text on HAL ]
[5] Sylvie Boldo and Jean-Christophe Filliâtre. Formal Verification of Floating-Point Programs. In 18th IEEE International Symposium on Computer Arithmetic, pages 187--194, Montpellier, France, June 2007. [ bib | PDF | .pdf ]
This paper introduces a methodology to perform formal verification of floating-point C programs. It extends an existing tool for the verification of C programs, Caduceus, with new annotations specific to floating-point arithmetic. The Caduceus first-order 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 floating-point arithmetic. This methodology is already implemented and has been successfully applied to several short floating-point programs, which are presented in this paper.

[4] Sylvie Boldo. Pitfalls of a full floating-point 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 52--66, 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 1328--1332, Dijon, France, April 2006. [ bib | full text on HAL ]
[2] Sylvie Boldo, Marc Daumas, William Kahan, and Guillaume Melquiond. Proof and certification for an accurate discriminant. In 12th IMACS-GAMM International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Duisburg,Germany, sep 2006. [ bib | http ]
[1] Sylvie Boldo and Jean-Michel Muller. Some functions computable with a fused-mac. In Paolo Montuschi and Eric Schwarz, editors, Proceedings of the 17th Symposium on Computer Arithmetic, pages 52--58, Cape Cod, USA, 2005. [ bib | .pdf ]

Back
This page was generated by bibtex2html.