Publications by year:
2020
| [BLM20] | Sylvie Boldo, Christoph Q. Lauter, and Jean-Michel Muller. Emulating round-to-nearest ties-to-zero ”augmented” floating-point operations using round-to-nearest ties-to-even arithmetic. IEEE Transactions on Computers, June 2020. Accepted for publication. [ bib | http | .pdf ] |
| [BGWH20] | Sylvie Boldo, Diane Gallois-Wong, and Thibault Hilaire. A Correctly-Rounded Fixed-Point-Arithmetic Dot-Product Algorithm. In Proceedings of the 27th Symposium on Computer Arithmetic (ARITH 2020), Portland, Oregon, June 2020. IEEE. [ bib ] |
| [GWBC20] | Diane Gallois-Wong, Sylvie Boldo, and Pascal Cuoq. Optimal Inverse Projection of Floating-Point Addition. Numerical Algorithms, 83(3):957--986, 2020. [ bib | DOI | http | .pdf ] |
2019
| [BL19] | Proceedings of the 26th Symposium on Computer Arithmetic (ARITH 2019), Kyoto, June 2019. IEEE. [ bib | DOI | http ] |
| [BFC19] | Sylvie Boldo, Florian Faissole, and Alexandre Chapoutot. Round-off error and exceptional behavior analysis of explicit Runge-Kutta methods. IEEE Transactions on Computers, 2019. [ bib | DOI | http ] |
2018
| [GWBH18] | Diane Gallois-Wong, Sylvie Boldo, and Thibault Hilaire. A Coq formalization of digital filters. In Florian Rabe, William M. Farmer, Grant O. Passmore, and Abdou Youssef, editors, CICM 2018 - 11th Conference on Intelligent Computer Mathematics, Intelligent Computer Mathematics, pages 87--103, Hagenberg, Austria, August 2018. [ bib | DOI | http | .pdf ] |
| [BFT18] | Sylvie Boldo, Florian Faissole, and Vincent Tourneur. A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers. In 25th IEEE Symposium on Computer Arithmetic, Amherst, MA, United States, June 2018. [ bib | DOI | http ] |
| [BM18] | Sylvie Boldo and Nicolas Magaud, editors. Journées Francophones des Langages Applicatifs 2018, Banyuls-sur-Mer, France, January 2018. [ bib | http | .pdf ] |
2017
| [BM17] | Sylvie Boldo and Guillaume Melquiond. Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the Coq System. ISTE Press - Elsevier, December 2017. [ bib ] |
| [BJMP17] | Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, and Valentina Popescu. Formal Verification of a Floating-Point Expansion Renormalization Algorithm. In 8th International Conference on Interactive Theorem Proving (ITP'2017), volume 10499 of Lecture Notes in Computer Science, Brasilia, Brazil, September 2017. [ bib | http | .pdf ] |
| [BFC17c] | 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 | http | .pdf ] |
| [AB17] | 10th International Workshop on Numerical Software Verification, France, July 2017. Springer. [ bib | http ] |
| [BGM17] | Sylvie Boldo, Stef Graillat, and Jean-Michel Muller. On the robustness of the 2Sum and Fast2Sum algorithms. ACM Transactions on Mathematical Software, 44(1), July 2017. [ bib | http | .pdf ] |
| [BCF17b] | 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 | http | .pdf ] |
| [BCF17a] | 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, Paris, France, January 2017. ACM. [ bib | DOI | http | .pdf ] |
| [BS17] | Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France, January 2017. [ bib | http ] |
2016
| [Bol16a] | 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 | http | .pdf ] |
| [Bol16b] | Sylvie Boldo. Iterators: where folds fail. In Workshop on High-Consequence Control Verification, Toronto, Canada, July 2016. [ bib | http | .pdf ] |
| [BLM16] | Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Formalization of Real Analysis: A Survey of Proof Assistants and Libraries. Mathematical Structures in Computer Science, 26(7):1196--1233, 2016. [ bib | http ] |
2015
| [Bol15b] | 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 International Publishing. [ bib | http | .pdf ] |
| [Bol15a] | 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 | http ] |
| [VBMB15] | Thierry Viéville, 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 | 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 ] |
| [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 ] |
2014
| [Bol14c] | Sylvie Boldo. Même les ordinateurs font des erreurs !, pages 136--137. Nouveau Monde Editions, October 2014. [ bib | http ] |
| [Bol14a] | Sylvie Boldo. Deductive Formal Verification: How To Make Your Floating-Point Programs Behave. Thèse d'habilitation, Université Paris-Sud, October 2014. [ bib | .pdf ] |
| [Bol14b] | 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 | http ] |
| [BolMul14] | Sylvie Boldo and Jean-Michel Muller. Des ordinateurs capables de calculer plus juste, pages 46--52. Number 492. October 2014. [ bib ] |
| [BCF14] | 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 | http ] |
2013
| [BM13] | 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 ] |
| [Bol13] | Sylvie Boldo. How to Compute the Area of a Triangle: a Formal Revisit. In Proceedings of the 21th IEEE Symposium on Computer Arithmetic, pages 91--98, Austin, Texas, USA, April 2013. [ bib | http ] |
| [BJLM13] | 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, pages 107--115, Austin, Texas, USA, April 2013. [ bib | http ] |
| [Mediation13] | 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 P. 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. Intern report, none, March 2013. [ 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 ] |
2012
| [BLM12] | 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 The Second International Conference on Certified Programs and Proofs, volume 7679 of Lecture Notes in Computer Science, pages 289--304, Kyoto, Japan, 2012. [ bib | DOI | http ] |
2011
| [BolVie11a] | Sylvie Boldo and Thierry Viéville. Introduction à la science informatique, chapter Représentation numérique de l’information, pages 23--72. Repères pour agir. CRDP Académie de Paris, July 2011. [ bib | http ] |
| [BolVie11b] | Sylvie Boldo and Thierry Viéville. Introduction à la science informatique, chapter Structuration et contrôle de l’information, pages 281--308. Repères pour agir. CRDP Académie de Paris, July 2011. [ bib | http ] |
| [BolMar11] | 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 | 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 ] |
| [BolMel11] | Sylvie Boldo and Guillaume Melquiond. Flocq: A Unified Library for Proving Floating-point Algorithms in Coq. In Proceedings of the 20th IEEE Symposium on Computer Arithmetic, pages 243--252, Tübingen, Germany, July 2011. [ bib ] |
2010
| [Bol10] | 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 | http ] |
| [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 Matt Kaufmann and Lawrence C. Paulson, editors, Proceedings of the first Interactive Theorem Proving Conference (ITP), volume 6172 of LNCS, pages 147--162, Edinburgh, Scotland, July 2010. Springer. (merge of TPHOL and ACL2). [ bib | http ] |
| [BolNgu10] | 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, number NASA/CP-2010-216215 in NASA Conference Publication, pages 14--23, Washington D.C., USA, April 2010. [ bib | .pdf ] |
| [Bol10_webtv] | Sylvie Boldo. L'informatique. Universcience web television, April 2010. Quiz 5-12. [ bib | .html ] |
| [Bol10_I1] | Sylvie Boldo. C'est la faute à l'ordinateur! Interstices -- Idée reçue, February 2010. [ bib | http ] |
| [Bol10_I2] | Sylvie Boldo. Un algorithme de découpe de gâteau. Interstices, July 2010. [ bib | http ] |
2009
| [BFM09] | 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 | .pdf ] |
| [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 ] |
| [RZBG09] | 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 | http ] |
| [Bol09_I] | Sylvie Boldo. Demandez le programme! Interstices, February 2009. [ bib | http ] |
| [BolDauLi09] | 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 | http ] |
| [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 ] |
2008
| [Bol08DS] | Sylvie Boldo. Demandez le programme!, volume 5, pages 26--33. C.R.D.P. de l'académie de Versailles, November 2008. [ bib | http ] |
| [Bol08_I2] | Sylvie Boldo. L'informatique, ce n'est pas pour les filles. Interstices, September 2008. [ bib | http ] |
| [Bol08_I1] | Sylvie Boldo. Pourquoi mon ordinateur calcule-t-il faux? Interstices, April 2008. Podcast. [ bib | http ] |
| [BolMel08] | 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 | http ] |
| [BolDauGio08] | Sylvie Boldo, Marc Daumas, and Pascal Giorgi. Formal proof for delayed finite field arithmetic using floating point operators. In Proceedings of the 8th Conference on Real Numbers and Computers, Santiago de Compostela, Spain, July 2008. [ bib | http ] |
2007
| [BolFil07] | Sylvie Boldo and Jean-Christophe Filliâtre. Formal Verification of Floating-Point Programs. In Peter Kornerup and Jean-Michel Muller, editors, Proceedings of the 18th IEEE Symposium on Computer Arithmetic, pages 187--194, Montpellier, France, June 2007. [ bib | DOI | .pdf ] |
2006
| [BDKM06] | 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, September 2006. [ bib | http ] |
| [Bol06a] | Sylvie Boldo. Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms. In Proceedings of the third International Joint Conference on Automated Reasoning (IJCAR), pages 52--66, Seattle, USA, August 2006. [ bib | DOI ] |
| [Bol06b] | Sylvie Boldo. Formal Proofs about DSPs. In Bruno Buchberger, Shin'ichi Oishi, Michael Plum, and Sigfried M. Rump, editors, Algebraic and Numerical Algorithms and Computer-assisted Proofs, number 05391 in Dagstuhl Seminar Proceedings, Dagstuhl, Germany, 2006. Internationales Begegnungs- und Forschungszentrum (IBFI), Schloss Dagstuhl, Germany. [ bib | .pdf ] |
| [BolMun06] | 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 | DOI | http ] |
2005
| [BolMul05] | 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 | DOI | .pdf ] |
| [BolMel05] | Sylvie Boldo and Guillaume Melquiond. When double rounding is odd. In Proceedings of the 17th IMACS World Congress, Scientific Computation, Applied Mathematics and Simulation, Paris, France, 2005. [ bib | http ] |
2004
| [Bol04b] | Sylvie Boldo. Preuves formelles en arithmétiques à virgule flottante. PhD thesis, École Normale Supérieure de Lyon, November 2004. [ bib | .pdf ] |
| [BolDau04a] | Sylvie Boldo and Marc Daumas. Properties of two's complement floating point notations. International Journal on Software Tools for Technology Transfer, 5(2-3):237--246, 2004. [ bib | DOI | http ] |
| [BolDau04b] | Sylvie Boldo and Marc Daumas. A simple test qualifying the accuracy of Horner's rule for polynomials. Numerical Algorithms, 37(1-4):45--60, 2004. [ bib | DOI | http ] |
| [Bol04a] | Sylvie Boldo. Bridging the gap between formal specification and bit-level floating-point arithmetic. In Christiane Frougny, Vasco Brattka, and Norbert Müller, editors, Proceedings of the 6th Conference on Real Numbers and Computers, pages 22--36, Schloss Dagstuhl, Germany, 2004. [ bib | .pdf ] |
2003
| [BolDauThe03] | Sylvie Boldo, Marc Daumas, and Laurent Théry. Formal proofs and computations in finite precision arithmetic. In Proceedings of the 11th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, pages 101--111, Roma, Italy, 2003. [ bib | .pdf ] |
| [LiBolDau03] | Ren-Cang Li, Sylvie Boldo, and Marc Daumas. Theorems on efficient argument reductions. In Jean-Claude Bajard and Michael Schulte, editors, Proceedings of the 16th Symposium on Computer Arithmetic, pages 129--136, Santiago de Compostela, Spain, 2003. [ bib | DOI | http ] |
| [BolDau03] | Sylvie Boldo and Marc Daumas. Representable correcting terms for possibly underflowing floating point operations. In Jean-Claude Bajard and Michael Schulte, editors, Proceedings of the 16th Symposium on Computer Arithmetic, pages 79--86, Santiago de Compostela, Spain, 2003. [ bib | DOI ] |
2002
| [BolDau02b] | Sylvie Boldo and Marc Daumas. Faithful rounding without fused multiply and accumulate. In Jean-Luc Lamotte and Fabien Rico, editors, Proceedings of the 10th IMACS-GAMM International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, page 161, Paris, France, 2002. [ bib ] |
| [BolDau02a] | Sylvie Boldo and Marc Daumas. Properties of the subtraction valid for any floating point system. In 7th International Workshop on Formal Methods for Industrial Critical Systems, pages 137--149, Málaga, Spain, 2002. Also in Electronic Notes in Theoretical Computer Science, volume 66(2). Elsevier, 2002. [ bib | DOI | .pdf ] |
| [Bol02] | Sylvie Boldo. Introduction à l'arithmétique des ordinateurs. In Forum des jeunes mathématiciennes et des jeunes informaticiennes, pages 7--10, Paris, France, 2002. [ bib ] |
2001
| [BolDau01b] | Sylvie Boldo and Marc Daumas. A mechanically validated technique for extending the available precision. In 35th Asilomar Conference on Signals, Systems, and Computers, pages 1299--1303, Pacific Grove, California, 2001. [ bib | DOI ] |
| [BolDau01a] | Sylvie Boldo and Marc Daumas. Performances d'implantations de l'addition en précision quad-double sur différentes machines. In 7ème Symposium sur les Architectures Nouvelles de Machines, pages 105--112, Paris, France, 2001. [ bib | .pdf ] |
This file was generated by bibtex2html 1.98.
