Sylvie Boldo

Q: What Schools Are Affiliated With Sylvie Boldo

Sylvie Boldo is affiliated with the following schools: Paris-Saclay University, École normale supérieure de Lyon

Sylvie Boldo's AcademicInfluence.com Rankings

Sylvie Boldo

Mathematics

#4433

World Rank

#6298

Historical Rank

Control Theory

#71

World Rank

#76

Historical Rank

Measure Theory

#3981

World Rank

#4691

Historical Rank

mathematics Degrees

Sylvie Boldo

Computer Science

#6938

World Rank

#7306

Historical Rank

Numerical Analysis

#58

World Rank

#62

Historical Rank

computer-science Degrees

Download Badge

Mathematics
Computer Science

Why Is Sylvie Boldo Influential?

(Suggest an Edit or Addition)

According to Wikipedia, Sylvie Boldo is a French mathematician and computer scientist. Her research combines automated theorem proving and computer arithmetic, focusing on the formal verification of floating-point arithmetic operations and of algorithms based on them. She is a director of research for the French Institute for Research in Computer Science and Automation , affiliated with the Formal Methods Laboratory at Paris-Saclay University and the INRIA Saclay-Île-de-France Research Centre, where she co-leads the Toccata project for formally verified programs, certified tools and numerical computations. She is also the founding jury president for the French agrégation in computer science.

(See a Problem?)

Sylvie Boldo's Published Works

Number of citations in a given year to any of this author's works

Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author

Published Works

IEEE Standard for Floating-Point Arithmetic (2008) (1446)
Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq (2011) (131)
Coquelicot: A User-Friendly Library of Real Analysis for Coq (2015) (109)
Formal Verification of Floating-Point Programs (2007) (106)
Combining Coq and Gappa for Certifying Floating-Point Programs (2009) (72)
Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program (2011) (70)
Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd (2008) (51)
A Formally-Verified C Compiler Supporting Floating-Point Arithmetic (2013) (50)
Formalization of real analysis: a survey of proof assistants and libraries † (2015) (49)
Representable correcting terms for possibly underflowing floating point operations (2003) (43)
Formal Proof of a Wave Equation Resolution Scheme: The Method Error (2010) (41)
Verified Compilation of Floating-Point Computations (2015) (38)
Trusting computations: A mechanized proof from partial differential equations to actual program (2012) (31)
Some functions computable with a fused-mac (2005) (31)
Theorems on efficient argument reductions (2003) (30)
Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms (2006) (28)
Hardware-independent Proofs of Numerical Programs (2010) (28)
Formal Verification of Numerical Programs: From C Annotated Programs to Mechanical Proofs (2011) (27)
A Simple Test Qualifying the Accuracy of Horner'S Rule for Polynomials (2004) (24)
When double rounding is odd (2005) (21)
A Coq formal proof of the Lax-Milgram theorem (2017) (21)
Computing predecessor and successor in rounding to nearest (2009) (20)
Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives (2012) (19)
Floats and Ropes: A Case Study for Formal Numerical Program Verification (2009) (17)
Exact and Approximated Error of the FMA (2011) (17)
Formally Verified Argument Reduction with a Fused Multiply-Add (2007) (16)
Computer Arithmetic and Formal Proofs - Verifying Floating-point Algorithms with the Coq System (2017) (15)
Proofs of numerical programs when the compiler optimizes (2011) (15)
Properties of two’s complement floating point notations (2004) (14)
On the Robustness of the 2Sum and Fast2Sum Algorithms (2017) (14)
Kahan's Algorithm for a Correct Discriminant Computation at Last Formally Proven (2009) (14)
Provably faithful evaluation of polynomials (2006) (13)
Floats & Ropes : a case study for formal numerical program veri cation ? (2009) (13)
A mechanically-validated technique for extending the available precision (2001) (12)
Computer Arithmetic and Formal Proofs (2017) (11)
A High-Level Formalization of Floating-Point Number in PVS (2006) (11)
Computer validated proofs of a toolset for adaptable arithmetic (2001) (10)
Deductive Formal Verification: How To Make Your Floating-Point Programs Behave (2014) (10)
Formal Verification of a Floating-Point Expansion Renormalization Algorithm (2017) (8)
Round-off Error Analysis of Explicit One-Step Numerical Integration Methods (2017) (8)
Properties of the subtraction valid for any floating point system (2002) (7)
A Coq Formalization of Lebesgue Integration of Nonnegative Functions (2021) (6)
How to Compute the Area of a Triangle: A Formal Revisit (2013) (5)
Optimal inverse projection of floating-point addition (2020) (5)
Deductive Program Verification (2017) (4)
Formal Verification of Programs Computing the Floating-Point Average (2015) (4)
A Coq Formalization of Digital Filters (2018) (4)
Round-Off Error and Exceptional Behavior Analysis of Explicit Runge-Kutta Methods (2020) (3)
A Coq Formalization of the Bochner integral (2022) (3)
Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number (2015) (2)
A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers (2018) (2)
Emulating Round-to-Nearest Ties-to-Zero “Augmented” Floating-Point Operations Using Round-to-Nearest Ties-to-Even Arithmetic (2021) (2)
Iterators: where folds fail (2016) (2)
Bridging the gap between formal specification and bit-level floating-point arithmetic (2004) (2)
Formal verification of tricky numerical computations (2014) (2)
Necessary and sufficient conditions for exact floating point operations (2002) (1)
A Correctly-Rounded Fixed-Point-Arithmetic Dot-Product Algorithm (2020) (1)
Des ordinateurs capables de calculer plus juste (2014) (1)
Lebesgue Induction and Tonelli's Theorem in Coq (2022) (1)
Some Formal Tools for Computer Arithmetic: Flocq and Gappa (2021) (1)
Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program (2012) (1)
Numerical Software Verification (2017) (1)
Formal verification of numerical programs: from C annotated programs to Coq proofs (2010) (1)
On the robustness of the 2Sum and Fast2Sum algorithms (2019) (0)
Wave Equation Numerical Resolution: Mathematics and Program (2011) (0)
Bounding the Round-Off Error of the Upwind Scheme for Advection (2022) (0)
10th International Workshop on Numerical Software Verification (2017) (0)
Computing a Correct and Tight Rounding Error Bound Using Rounding-to-Nearest (2016) (0)
Error-Free Computations and Applications (2017) (0)
Formal proofs of numerical programs (2010) (0)
Formalization of Formats and Basic Operators (2017) (0)
Proceedings of the 26th Symposium on Computer Arithmetic (ARITH 2019) (2019) (0)
Optimal inverse projection of floating-point addition (2019) (0)
Software - The Flocq library (2010) (0)
Software and Platforms - The Coquelicot library for real analysis (2013) (0)
Coquelicot: A User-Friendly Library of Real Analysis for Coq (2014) (0)
NASA / CR-2006-214298 NIA Report No . 2006-01 A High-Level Formalization of Floating-Point Number s in PVS (2006) (0)
Verified Compilation of Floating-Point Computations (2014) (0)
Bounding the Round-Off Error of the Upwind Scheme for Advection (2022) (0)
Necessary and sufficient conditions for exact floating point operations 1 Necessary and sufficient conditions for exact floating point operations 1 (2006) (0)
Necessary and sufficient conditions for exact floating point operations 1 Necessary and sufficient conditions for exact floating point operations 1 (2006) (0)
The Coq System (2017) (0)
Compilation of FP Programs (2017) (0)
New Results - Proof of imperative and object-oriented programs (2006) (0)
Real and Numerical Analysis (2017) (0)
Scientific Foundations - Higher-Order Functional Languages (2010) (0)
Scientific Foundations - Proof of Imperative andObject-Oriented programs (2011) (0)
Argument Reduction with a Fused Multiply-Add (2009) (0)
Other Grants and Activities - National initiatives (2010) (0)
A Coq Formalization of Lebesgue Induction Principle and Tonelli's Theorem (2023) (0)
Example Proofs of Advanced Operators (2017) (0)
Software and Platforms - The Flocq library (2013) (0)
Other Grants and Activities - Regional Initiatives (2010) (0)

This paper list is powered by the following services:

Other Resources About Sylvie Boldo

en.wikipedia.org

What Schools Are Affiliated With Sylvie Boldo?

Sylvie Boldo is affiliated with the following schools:

Sylvie Boldo's Academic­Influence.com Rankings

Why Is Sylvie Boldo Influential?

Sylvie Boldo's Published Works

Published Works

Other Resources About Sylvie Boldo

What Schools Are Affiliated With Sylvie Boldo?

Sylvie Boldo's AcademicInfluence.com Rankings