Sylvie Boldo - RankMe

61 papers A 1B 5C 16Misc 1Journal 29Unranked 6

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	A Rocq Formalization of Monomial and Graded Orders. CoRR Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero
2024	—	`conf`	Teaching Divisibility and Binomials with Coq. ThEdu@CADE Sylvie Boldo, François Clément, David Hamelin, Micaela Mayero, Pierre Rousselin
2023	B	`conf`	A Coq Formalization of Lebesgue Induction Principle and Tonelli's Theorem. FM Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine
2023	J	`jnl`	Floating-point arithmetic. Acta Numer. Sylvie Boldo, Claude-Pierre Jeannerod, Guillaume Melquiond, Jean-Michel Muller
2022	J	`jnl`	A Coq Formalization of Lebesgue Integration of Nonnegative Functions. J. Autom. Reason. Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
2022	J	`jnl`	A Coq Formalization of the Bochner integral. CoRR Sylvie Boldo, François Clément, Louise Leclerc
2022	C	`conf`	Bounding the Round-Off Error of the Upwind Scheme for Advection. ARITH Louise Ben Salem-Knapp, Sylvie Boldo, William Weens
2022	J	`jnl`	Bounding the Round-Off Error of the Upwind Scheme for Advection. IEEE Trans. Emerg. Top. Comput. Louise Ben Salem-Knapp, Sylvie Boldo, William Weens
2022	J	`jnl`	Lebesgue Induction and Tonelli's Theorem in Coq. CoRR Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine
2021	J	`jnl`	A Coq Formalization of Lebesgue Integration of Nonnegative Functions. CoRR Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
2021	J	`jnl`	Emulating Round-to-Nearest Ties-to-Zero "Augmented" Floating-Point Operations Using Round-to-Nearest Ties-to-Even Arithmetic. IEEE Trans. Computers Sylvie Boldo, Christoph Quirin Lauter, Jean-Michel Muller
2021	C	`conf`	Some Formal Tools for Computer Arithmetic: Flocq and Gappa. ARITH Sylvie Boldo, Guillaume Melquiond
2020	C	`conf`	A Correctly-Rounded Fixed-Point-Arithmetic Dot-Product Algorithm. ARITH Sylvie Boldo, Diane Gallois-Wong, Thibault Hilaire
2020	J	`jnl`	Optimal inverse projection of floating-point addition. Numer. Algorithms Diane Gallois-Wong, Sylvie Boldo, Pascal Cuoq
2020	J	`jnl`	Round-Off Error and Exceptional Behavior Analysis of Explicit Runge-Kutta Methods. IEEE Trans. Computers Sylvie Boldo, Florian Faissole, Alexandre Chapoutot
2019	C	`ed.`	26th IEEE Symposium on Computer Arithmetic, ARITH 2019, Kyoto, Japan, June 10-12, 2019 ARITH Naofumi Takagi, Sylvie Boldo, Martin Langhammer
2018	C	`conf`	A Coq Formalization of Digital Filters. CICM Diane Gallois-Wong, Sylvie Boldo, Thibault Hilaire
2018	C	`conf`	A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers. ARITH Sylvie Boldo, Florian Faissole, Vincent Tourneur
2017	B	`conf`	A Coq formal proof of the LaxMilgram theorem. CPP Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
2017	—	`book`	Computer Arithmetic and Formal Proofs - Verifying Floating-point Algorithms with the Coq System. Sylvie Boldo, Guillaume Melquiond
2017	B	`conf`	Formal Verification of a Floating-Point Expansion Renormalization Algorithm. ITP Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, Valentina Popescu
2017	—	`ed.`	Numerical Software Verification - 10th International Workshop, NSV 2017, Heidelberg, Germany, July 22-23, 2017, Proceedings [collocated with CAV 2017] NSV@CAV Alessandro Abate, Sylvie Boldo
2017	J	`jnl`	On the Robustness of the 2Sum and Fast2Sum Algorithms. ACM Trans. Math. Softw. Sylvie Boldo, Stef Graillat, Jean-Michel Muller
2017	C	`conf`	Round-off Error Analysis of Explicit One-Step Numerical Integration Methods. ARITH Sylvie Boldo, Florian Faissole, Alexandre Chapoutot
2016	—	`conf`	Computing a Correct and Tight Rounding Error Bound Using Rounding-to-Nearest. NSV@CAV Sylvie Boldo
2016	J	`jnl`	Formalization of real analysis: a survey of proof assistants and libraries. Math. Struct. Comput. Sci. Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
2015	J	`jnl`	Coquelicot: A User-Friendly Library of Real Analysis for Coq. Math. Comput. Sci. Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
2015	C	`conf`	Formal Verification of Programs Computing the Floating-Point Average. ICFEM Sylvie Boldo
2015	J	`jnl`	Verified Compilation of Floating-Point Computations. J. Autom. Reason. Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
2014	—	`book`	Deductive Formal Verification: How To Make Your Floating-Point Programs Behave. Sylvie Boldo
2014	—	`conf`	Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number. NSV Sylvie Boldo
2014	J	`jnl`	Trusting computations: A mechanized proof from partial differential equations to actual program. Comput. Math. Appl. Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2013	C	`conf`	A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. IEEE Symposium on Computer Arithmetic Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
2013	C	`conf`	How to Compute the Area of a Triangle: A Formal Revisit. IEEE Symposium on Computer Arithmetic Sylvie Boldo
2013	J	`jnl`	Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program. J. Autom. Reason. Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2012	B	`conf`	Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives. CPP Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
2012	J	`jnl`	Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program. CoRR Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2011	J	`jnl`	Exact and Approximated Error of the FMA. IEEE Trans. Computers Sylvie Boldo, Jean-Michel Muller
2011	C	`conf`	Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq. IEEE Symposium on Computer Arithmetic Sylvie Boldo, Guillaume Melquiond
2011	J	`jnl`	Formal Verification of Numerical Programs: From C Annotated Programs to Mechanical Proofs. Math. Comput. Sci. Sylvie Boldo, Claude Marché
2011	J	`jnl`	Proofs of numerical programs when the compiler optimizes. Innov. Syst. Softw. Eng. Sylvie Boldo, Thi Minh Tuyen Nguyen
2011	J	`jnl`	Wave Equation Numerical Resolution: Mathematics and Program CoRR Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2010	B	`conf`	Formal Proof of a Wave Equation Resolution Scheme: The Method Error. ITP Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2010	J	`jnl`	Formal Proof of a Wave Equation Resolution Scheme: the Method Error CoRR Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
2010	—	`conf`	Hardware-independent Proofs of Numerical Programs. NASA Formal Methods Sylvie Boldo, Thi Minh Tuyen Nguyen
2009	—	`conf`	Combining Coq and Gappa for Certifying Floating-Point Programs. Calculemus/MKM Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond
2009	—	`conf`	Floats and Ropes: A Case Study for Formal Numerical Program Verification. ICALP (2) Sylvie Boldo
2009	J	`jnl`	Formally Verified Argument Reduction with a Fused Multiply-Add. IEEE Trans. Computers Sylvie Boldo, Marc Daumas, Ren-Cang Li
2009	J	`jnl`	Kahan's Algorithm for a Correct Discriminant Computation at Last Formally Proven. IEEE Trans. Computers Sylvie Boldo
2008	J	`jnl`	Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd. IEEE Trans. Computers Sylvie Boldo, Guillaume Melquiond
2007	C	`conf`	Formal Verification of Floating-Point Programs. IEEE Symposium on Computer Arithmetic Sylvie Boldo, Jean-Christophe Filliâtre
2007	J	`jnl`	Formally Verified Argument Reduction with a Fused-Multiply-Add CoRR Sylvie Boldo, Marc Daumas, Ren-Cang Li
2006	A	`conf`	Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms. IJCAR Sylvie Boldo
2006	Misc	`conf`	Provably faithful evaluation of polynomials. SAC Sylvie Boldo, César A. Muñoz
2005	C	`conf`	Some Functions Computable with a Fused-Mac. IEEE Symposium on Computer Arithmetic Sylvie Boldo, Jean-Michel Muller
2004	J	`jnl`	A Simple Test Qualifying the Accuracy of Horner'S Rule for Polynomials. Numer. Algorithms Sylvie Boldo, Marc Daumas
2004	J	`jnl`	Properties of two's complement floating point notations. Int. J. Softw. Tools Technol. Transf. Sylvie Boldo, Marc Daumas
2003	C	`conf`	Representable Correcting Terms for Possibly Underflowing Floating Point Operations. IEEE Symposium on Computer Arithmetic Sylvie Boldo, Marc Daumas
2003	C	`conf`	Theorems on Efficient Argument Reductions. IEEE Symposium on Computer Arithmetic Ren-Cang Li, Sylvie Boldo, Marc Daumas
2002	C	`conf`	Properties of the subtraction valid for any floating point system. FMICS Sylvie Boldo, Marc Daumas
2001	J	`jnl`	Computer validated proofs of a toolset for adaptable arithmetic CoRR Sylvie Boldo, Marc Daumas, Claire Moreau-Finot, Laurent Théry