Search

Your search keyword '"Sylvie Boldo"' showing total 97 results
Start Over Author "Sylvie Boldo"
97 results on '"Sylvie Boldo"'

7. Floating-point arithmetic

Author

Sylvie Boldo, Claude-Pierre Jeannerod, Guillaume Melquiond, Jean-Michel Muller, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Arithmétiques des ordinateurs, méthodes formelles, génération de code (ARIC), Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Lyon, Institut National de Recherche en Informatique et en Automatique (Inria), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS), ANR-20-CE48-0014,NuSCAP,Sûreté numérique pour les preuves assistées par ordinateur(2020), and European Project: 810367,EMC2(2019)

Subjects
computer arithmetic, Numerical Analysis, [INFO.INFO-AO]Computer Science [cs]/Computer Arithmetic, General Mathematics, Floating-point arithmetic, numerical computing
Abstract

Floating-point numbers have an intuitive meaning when it comes to physics-based numerical computations, and they have thus become the most common way of approximating real numbers in computers. The IEEE-754 Standard has played a large part in making floating-point arithmetic ubiquitous today, by specifying its semantics in a strict yet useful way as early as 1985. In particular, floating-point operations should be performed as if their results were first computed with an infinite precision and then rounded to the target format. A consequence is that floating-point arithmetic satisfies the ‘standard model’ that is often used for analysing the accuracy of floating-point algorithms. But that is only scraping the surface, and floating-point arithmetic offers much more.In this survey we recall the history of floating-point arithmetic as well as its specification mandated by the IEEE-754 Standard. We also recall what properties it entails and what every programmer should know when designing a floating-point algorithm. We provide various basic blocks that can be implemented with floating-point arithmetic. In particular, one can actually compute the rounding error caused by some floating-point operations, which paves the way to designing more accurate algorithms. More generally, properties of floating-point arithmetic make it possible to extend the accuracy of computations beyond working precision.

Published
2023

28. A Coq Formalization of Lebesgue Integration of Nonnegative Functions

Author

François Clément, Vincent Martin, Sylvie Boldo, Micaela Mayero, Florian Faissole, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Simulation for the Environment: Reliable and Efficient Numerical Algorithms (SERENA), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre d'Enseignement et de Recherche en Mathématiques et Calcul Scientifique (CERMICS), École des Ponts ParisTech (ENPC), Laboratoire de Mathématiques Appliquées de Compiègne (LMAC), Université de Technologie de Compiègne (UTC), Laboratoire d'Informatique de Paris-Nord (LIPN), Centre National de la Recherche Scientifique (CNRS)-Université Sorbonne Paris Nord, This work was partly supported by the Paris Île-de-France Region (DIM RFSI MILC). This work was partly supported by Labex DigiCosme (project ANR-11-LABEX-0045-DIGICOSME) operated by ANR as part of the program 'Investissement d’Avenir' Idex Paris-Saclay (ANR-11-IDEX-0003-02). This work was partly supported by the European Research Council (ERC) under the EuropeanUnion’s Horizon 2020 Research and Innovation Programme – Grant Agreement n◦810367., ANR-11-LABX-0045,DIGICOSME,Mondes numériques: Données, programmes et architectures distribués(2011), ANR-11-IDEX-0003,IPS,Idex Paris-Saclay(2011), and European Project: 810367,EMC2(2019)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Correctness, Measurable function, Lebesgue integration, 0102 computer and information sciences, 02 engineering and technology, [MATH.MATH-CA]Mathematics [math]/Classical Analysis and ODEs [math.CA], Mathematical proof, [MATH.MATH-FA]Mathematics [math]/Functional Analysis [math.FA], 01 natural sciences, Formal proof, symbols.namesake, Artificial Intelligence, formal proof, FOS: Mathematics, 0202 electrical engineering, electronic engineering, information engineering, Coq, Mathematics, Lemma (mathematics), Real analysis, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, Logic in Computer Science (cs.LO), Functional Analysis (math.FA), Algebra, Mathematics - Functional Analysis, measure theory, Computational Theory and Mathematics, 010201 computation theory & mathematics, Simple function, symbols, Software
Abstract

Integration, just as much as differentiation, is a fundamental calculus tool that is widely used in many scientific domains. Formalizing the mathematical concept of integration and the associated results in a formal proof assistant helps in providing the highest confidence on the correctness of numerical programs involving the use of integration, directly or indirectly. By its capability to extend the (Riemann) integral to a wide class of irregular functions, and to functions defined on more general spaces than the real line, the Lebesgue integral is perfectly suited for use in mathematical fields such as probability theory, numerical mathematics, and real analysis. In this article, we present the Coq formalization of $$\sigma $$ -algebras, measures, simple functions, and integration of nonnegative measurable functions, up to the full formal proofs of the Beppo Levi (monotone convergence) theorem and Fatou’s lemma. More than a plain formalization of the known literature, we present several design choices made to balance the harmony between mathematical readability and usability of Coq theorems. These results are a first milestone toward the formalization of $$L^p$$ spaces such as Banach spaces.

Published
2022

30. Bounding the Round-Off Error of the Upwind Scheme for Advection

Author

Louise Ben Salem-Knapp, Sylvie Boldo, William Weens, CEA,DAM,DIF, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire en Informatique Haute Performance pour le Calcul et la simulation (LIHPC), DAM Île-de-France (DAM/DIF), Direction des Applications Militaires (DAM), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Direction des Applications Militaires (DAM), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay, Laboratoire de Détection et de Géophysique (CEA) (LDG), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA), ANR-20-CE48-0014,NuSCAP,Sûreté numérique pour les preuves assistées par ordinateur(2020), and European Project: 810367,EMC2(2019)

Subjects
Human-Computer Interaction, [INFO.INFO-AO]Computer Science [cs]/Computer Arithmetic, Computer Science (miscellaneous), Advection, Hydrodynamics, Round-off error, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Computer Science Applications, Information Systems, Floating-Point, Numerical Scheme
Abstract

International audience; Numerical simulations are carefully-written programs, and their correctness is based on mathematical results. Nevertheless, those programs rely on floating-point arithmetic and the corresponding round-off errors are often ignored. This article deals with a specific simple scheme applied to advection, that is a particular equation from hydrodynamics dedicated to the transport of a substance. It shows a tight bound on the round-off error of the 1D and 2D upwind scheme, with an error roughly proportional to the number of steps. The error bounds are generic with respect to the format and exceptional behaviors are taken into account. Some experiments give an insight of the quality of the bounds.

Published
2021

31. Some Formal Tools for Computer Arithmetic: Flocq and Gappa

Author

Guillaume Melquiond, Sylvie Boldo, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Mioara Joldes, Fabrizio Lamberti, ANR-20-CE48-0014,NuSCAP,Sûreté numérique pour les preuves assistées par ordinateur(2020), and European Project: 810367,EMC2(2019)

Subjects
Floating point, Computer science, Formal methods, [INFO.INFO-AO]Computer Science [cs]/Computer Arithmetic, Proof assistant, Process (computing), [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Floating-point arithmetic, Mathematical proof, Formal proof, symbols.namesake, Taylor series, symbols, Round-off error, Coq, Arithmetic
Abstract

International audience; This invited paper presents two tools developed by the authors. Their purpose is to help the user in writing proofs regarding computer arithmetic, e.g., certifying a bound on a round-off error, while aiming at a high level of guarantee. Flocq is a library of mathematical definitions and theorems for the Coq proof assistant; Gappa is meant to compute bounds of values and errors, while producing the corresponding formal proof. We describe here these tools, how they interact and how they fit in a larger verification process.

Published
2021

32. Emulating round-to-nearest ties-to-zero 'augmented' floating-point operations using round-to-nearest ties-to-even arithmetic

Author

Jean-Michel Muller, Christoph Lauter, Sylvie Boldo, Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), University of Alaska [Anchorage], Université de Lyon, Arithmetic and Computing (ARIC), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Centre National de la Recherche Scientifique (CNRS), Laboratoire de l'Informatique du Parallélisme (LIP), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), ANR-14-CE25-0018,Fast Relax,Fast Reliable Approximation(2014), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), ANR-14-CE25-0018,Fast Relax,Approximation rapide et fiable(2014), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), and Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL)

Subjects
Correctness, Floating point, Computer science, ACM: G.: Mathematics of Computing/G.1: NUMERICAL ANALYSIS/G.1.0: General/G.1.0.0: Computer arithmetic, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], Binary number, 02 engineering and technology, Formal proof, Theoretical Computer Science, Error analysis, Error-free transforms, 0202 electrical engineering, electronic engineering, information engineering, Arithmetic, Numerical repro- ducibility, Rounding, [INFO.INFO-AO]Computer Science [cs]/Computer Arithmetic, Floating-point arithmetic, Rounding mode, IEEE floating point, 020202 computer hardware & architecture, Zero (linguistics), Rounding error analysis, Numerical reproducibility, Computational Theory and Mathematics, Hardware and Architecture, Software
Abstract

International audience; The 2019 version of the IEEE 754 Standard for Floating-Point Arithmetic recommends that new “augmented” operations should be provided for the binary formats. These operations use a new “rounding direction”: round to nearest ties-to-zero. We show how they can be implemented using the currently available operations, using round-to-nearest ties-to-even with a partial formal proof of correctness.

Published
2020

33. Optimal Inverse Projection of Floating-Point Addition

Author

Pascal Cuoq, Diane Gallois-Wong, Sylvie Boldo, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire de Recherche en Informatique (LRI), CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS), and TrustInSoft (TIS )

Subjects
Floating point, Applied Mathematics, Computation, Numerical analysis, [INFO.INFO-AO]Computer Science [cs]/Computer Arithmetic, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 010103 numerical & computational mathematics, Abstract interpretation, 01 natural sciences, Inverse projection, IEEE floating point, 010101 applied mathematics, Theory of computation, Local consistency, Applied mathematics, 0101 mathematics, Mathematics
Abstract

International audience; In a setting where we have intervals for the values of floating-point variables x, a, and b, we are interested in improving these intervals when the floating-point equality $x ⊕ a = $b holds. This problem is common in constraint propagation, and called the inverse projection of the addition. It also appears in abstract interpretation for the analysis of programs containing IEEE 754 operations. We propose floating-point theorems that provide optimal bounds for all the intervals. Fast loop-free algorithms compute these optimal bounds using only floating-point computations at the target precision.

Published
2020

34. Foreword

Author

Martin Langhammer and Sylvie Boldo

Subjects
Computer science, Arithmetic
Published
2019

35. Round-off error and exceptional behavior analysis of explicit Runge-Kutta methods

Author

Sylvie Boldo, Florian Faissole, Alexandre Chapoutot, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Unité d'Informatique et d'Ingénierie des Systèmes (U2IS), École Nationale Supérieure de Techniques Avancées (ENSTA Paris), and ANR-14-CE25-0018,Fast Relax,Approximation rapide et fiable(2014)

Subjects
Arithmetic underflow, Dynamical systems theory, Computer science, Numerical analysis, [INFO.INFO-AO]Computer Science [cs]/Computer Arithmetic, MathematicsofComputing_NUMERICALANALYSIS, 02 engineering and technology, 020202 computer hardware & architecture, Theoretical Computer Science, Numerical integration, Runge–Kutta methods, Underflow, Computational Theory and Mathematics, Hardware and Architecture, Ordinary differential equation, Overflow, 0202 electrical engineering, electronic engineering, information engineering, Applied mathematics, Runge-Kutta method, Round-off error, Linear stability, Software, Numerical stability
Abstract

International audience; Numerical integration schemes are mandatory to understand complex behaviors of dynamical systems described by ordinary differential equations. Implementation of these numerical methods involve floating-point computations and propagation of round-off errors. This paper presents a new fine-grained analysis of round-off errors in explicit Runge-Kutta integration methods, taking into account exceptional behaviors, such as underflow and overflow. Linear stability properties play a central role in the proposed approach. For a large class of Runge-Kutta methods applied on linear problems, a tight bound of the round-off errors is provided. A simple test is defined and ensures the absence of underflow and a tighter round-off error bound. The absence of overflow is guaranteed as linear stability properties imply that (computed) solutions are non-increasing.

Published
2019

36. A Coq formalization of digital filters

Author

Thibault Hilaire, Diane Gallois-Wong, Sylvie Boldo, Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Performance et Qualité des Algorithmes Numériques (PEQUAN), LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Florian Rabe, William M. Farmer, Grant O. Passmore, Abdou Youssef, CentraleSupélec-Université Paris-Sud - Paris 11 (UP11)-Centre National de la Recherche Scientifique (CNRS), CentraleSupélec-Université Paris-Sud - Paris 11 (UP11)-Centre National de la Recherche Scientifique (CNRS)-CentraleSupélec-Université Paris-Sud - Paris 11 (UP11)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Laboratoire de Recherche en Informatique ( LRI ), Université Paris-Sud - Paris 11 ( UP11 ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -CentraleSupélec-Centre National de la Recherche Scientifique ( CNRS ), Certified Programs, Certified Tools, Certified Floating-Point Computations ( TOCCATA ), Université Paris-Sud - Paris 11 ( UP11 ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -CentraleSupélec-Centre National de la Recherche Scientifique ( CNRS ) -Université Paris-Sud - Paris 11 ( UP11 ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -CentraleSupélec-Centre National de la Recherche Scientifique ( CNRS ) -Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique ( Inria ), Performance et Qualité des Algorithmes Numériques ( PEQUAN ), Laboratoire d'Informatique de Paris 6 ( LIP6 ), and Université Pierre et Marie Curie - Paris 6 ( UPMC ) -Centre National de la Recherche Scientifique ( CNRS ) -Université Pierre et Marie Curie - Paris 6 ( UPMC ) -Centre National de la Recherche Scientifique ( CNRS )

Subjects
0209 industrial biotechnology, Signal processing, business.industry, Computer science, [INFO.INFO-AO]Computer Science [cs]/Computer Arithmetic, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 0102 computer and information sciences, 02 engineering and technology, Filter (signal processing), 01 natural sciences, [ INFO.INFO-AO ] Computer Science [cs]/Computer Arithmetic, 020901 industrial engineering & automation, 010201 computation theory & mathematics, Control theory, Application domain, [ INFO.INFO-LO ] Computer Science [cs]/Logic in Computer Science [cs.LO], State (computer science), business, Digital filter, Equivalence (measure theory), Algorithm, Digital signal processing
Abstract

International audience; Digital filters are small iterative algorithms, used as basic bricks in signal processing (filters) and control theory (controllers). They receive as input a stream of values, and output another stream of values, computed from their internal state and from the previous inputs. These systems can be found in communication, aeronautics, automotive, robotics, etc. As the application domain may be critical, we aim at providing a formal guarantee of the good behavior of these algorithms in time-domain. In particular, we formally proved in Coq some error analysis theorems about digital filters, namely the Worst-Case Peak Gain theorem and the existence of a filter characterizing the difference between the exact filter and the implemented one. Moreover, the digital signal processing literature provides us with many equivalent algorithms, called realizations. We formally defined and proved the equivalence of several realizations (Direct Forms and State-Space).

Published
2018

37. A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers

Author

Vincent Tourneur, Florian Faissole, Sylvie Boldo, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Laboratoire de Recherche et de Développement de l'EPITA (LRDE), Ecole Pour l'Informatique et les Techniques Avancées (EPITA), ANR-14-CE25-0018,Fast Relax,Approximation rapide et fiable(2014), and ANR-11-LABX-0045,DIGICOSME,Mondes numériques: Données, programmes et architectures distribués(2011)

Subjects
Arithmetic underflow, Computer science, Computation, Rounding, [INFO.INFO-AO]Computer Science [cs]/Computer Arithmetic, Decimal floating point, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Radix, Hardware_ARITHMETICANDLOGICSTRUCTURES, Algorithm, Formal proof, Decimal
Abstract

International audience; Some modern processors include decimal floating-point units, with a conforming implementation of the IEEE-754 2008 standard. Unfortunately, many algorithms from the computer arithmetic literature are not correct anymore when computations are done in radix 10. This is in particular the case for the computation of the average of two floating-point numbers. Several radix-2 algorithms are available, including one that provides the correct rounding, but none hold in radix 10. This paper presents a new radix-10 algorithm that computes the correctly-rounded average. To guarantee a higher level of confidence, we also provide a Coq formal proof of our theorems, that takes gradual underflow into account. Note that our formal proof was generalized to ensure this algorithm is correct when computations are done with any even radix.

Published
2018

38. Computer Arithmetic and Formal Proofs : Verifying Floating-point Algorithms with the Coq System

Author

Sylvie Boldo, Guillaume Melquiond, Sylvie Boldo, and Guillaume Melquiond

Subjects
Floating-point arithmetic, Computer arithmetic, Computer algorithms
Abstract

Floating-point arithmetic is ubiquitous in modern computing, as it is the tool of choice to approximate real numbers. Due to its limited range and precision, its use can become quite involved and potentially lead to numerous failures. One way to greatly increase confidence in floating-point software is by computer-assisted verification of its correctness proofs. This book provides a comprehensive view of how to formally specify and verify tricky floating-point algorithms with the Coq proof assistant. It describes the Flocq formalization of floating-point arithmetic and some methods to automate theorem proofs. It then presents the specification and verification of various algorithms, from error-free transformations to a numerical scheme for a partial differential equation. The examples cover not only mathematical algorithms but also C programs as well as issues related to compilation. - Describes the notions of specification and weakest precondition computation and their practical use - Shows how to tackle algorithms that extend beyond the realm of simple floating-point arithmetic - Includes real analysis and a case study about numerical analysis

Published
2017

39. Numerical Software Verification : 10th International Workshop, NSV 2017, Heidelberg, Germany, July 22-23, 2017, Proceedings

Author

Alessandro Abate, Sylvie Boldo, Alessandro Abate, and Sylvie Boldo

Subjects
Computer science, Software engineering, Algorithms, Machine theory, Computer simulation
Abstract

This book constitutes the proceedings of the 10th International Workshop on Numerical Software Verification, NSV 2017, held in Heidelberg, Germany, in July 2017 - colocated with the International Workshop on Formal Methods for Rigorous Systems Engineering of Cyber-Physical Systems, RISE4CPS 2017, a one-time, invited-only event.The 3 full papers presented together with 3 short papers, 2 keynote abstracts and 4 invited abstracts were carefully reviewed and selected from numerous submissions.The NSV 2017 workshop is dedicated to the development of logical and mathematical techniques for the reasoning about programmability and reliability.

Published
2017

40. On the robustness of the 2Sum and Fast2Sum algorithms

Author

Stef Graillat, Jean-Michel Muller, Sylvie Boldo, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Performance et Qualité des Algorithmes Numériques (PEQUAN), Laboratoire d'Informatique de Paris 6 (LIP6), Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS), Arithmetic and Computing (ARIC), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Centre National de la Recherche Scientifique (CNRS), ANR-14-CE25-0018,Fast Relax,Approximation rapide et fiable(2014), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), and Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL)

Subjects
Kahan summation algorithm, faithful rounding, Floating point, Applied Mathematics, Rounding, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], 2Sum, Fast2Sum, 010103 numerical & computational mathematics, 02 engineering and technology, 01 natural sciences, error-free transformation, ACM: G.: Mathematics of Computing, 020202 computer hardware & architecture, Robustness (computer science), 0202 electrical engineering, electronic engineering, information engineering, rounding errors, Numerical computing, 0101 mathematics, Round-off error, floating-point, Algorithm, Software, Mathematics
Abstract

The 2Sum and Fast2Sum algorithms are important building blocks in numerical computing. They are used (implicitely or explicitely) in many compensated algorithms (such as compensated summation or compensated polynomial evaluation). They are also used for manipulating floating-point expansions . We show that these algorithms are much more robust than it is usually believed: The returned result makes sense even when the rounding function is not round-to-nearest, and they are almost immune to overflow.

Published
2017

41. A Coq formal proof of the Lax–Milgram theorem

Author

Florian Faissole, Vincent Martin, François Clément, Sylvie Boldo, Micaela Mayero, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Simulation for the Environment: Reliable and Efficient Numerical Algorithms (SERENA), Inria de Paris, Laboratoire de Mathématiques Appliquées de Compiègne (LMAC), Université de Technologie de Compiègne (UTC), Laboratoire d'Informatique de Paris-Nord (LIPN), Université Paris 13 (UP13)-Institut Galilée-Université Sorbonne Paris Cité (USPC)-Centre National de la Recherche Scientifique (CNRS), Labex Digicosme, and Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Babuška–Lax–Milgram theorem, Computer science, finite element method, Lax-Milgram theorem, 0102 computer and information sciences, 02 engineering and technology, [MATH.MATH-FA]Mathematics [math]/Functional Analysis [math.FA], 01 natural sciences, Formal proof, functional analysis, symbols.namesake, Lions–Lax–Milgram theorem, 020204 information systems, Completeness (order theory), formal proof, 0202 electrical engineering, electronic engineering, information engineering, Calculus, Coq, Uniqueness, Soundness, Hilbert space, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 010201 computation theory & mathematics, Linear algebra, symbols, [MATH.MATH-NA]Mathematics [math]/Numerical Analysis [math.NA]
Abstract

International audience; The Finite Element Method is a widely-used method to solve numerical problems coming for instance from physics or biology. To obtain the highest confidence on the correction of numerical simulation programs implementing the Finite Element Method, one has to formalize the mathematical notions and results that allow to establish the sound-ness of the method. The Lax–Milgram theorem may be seen as one of those theoretical cornerstones: under some completeness and coercivity assumptions, it states existence and uniqueness of the solution to the weak formulation of some boundary value problems. This article presents the full formal proof of the Lax–Milgram theorem in Coq. It requires many results from linear algebra, geometry, functional analysis , and Hilbert spaces.

Published
2017

42. Example Proofs of Advanced Operators

Author

Guillaume Melquiond and Sylvie Boldo

Subjects
EFTS, Lossless compression, Theoretical computer science, Computer science, Computation, Cover (algebra), Variety (universal algebra), Control (linguistics), Mathematical proof
Abstract

Has covered error-free transformations (EFTs) and lossless computations. In this chapter, the considered operators get more complicated. We can no longer get rid of inaccuracies, so the goal is to reduce them or to control them. The purpose of this chapter is twofold: first, to give more guarantees on advanced operators of the literature, potentially useful to the reader; second, to cover a variety of techniques and concerns when verifying FP algorithms. This is why the proofs are not detailed much (compared to the first chapters) and only the prominent points (such as case distinctions, difficulties, and peculiar definitions) are given.

Published
2017

43. Deductive Program Verification

Author

Sylvie Boldo and Guillaume Melquiond

Subjects
Correctness, Ideal (set theory), Programming language, Computer science, Computation, Value (computer science), Compiler, computer.software_genre, computer, Toolchain
Abstract

Have described several algorithms that perform FP computations and have shown how to formally verify their correctness (e.g. the computed value is close enough to the ideal value). Has presented a C compiler and the proof that it compiles FP operations in a way that does not invalidate the correctness of a C program. Now we are interested in the last piece of the puzzle, that is, proving the correctness of a C program and not just of the corresponding algorithm. First motivates program verification and explains how it differs from algorithm verification as done in previous chapters. We rely here on deductive verification and the toolchain we use for the examples of this chapter is Frama-C/Jessie/Why3; more information on the corresponding methodology is given. Then presents several examples of C programs. Most of them have been previously described, such as the area of a triangle or the average of two numbers. Finally, presents an alternative for ensuring that, whatever the compiler decisions about FP arithmetic, the compiled programs behave as specified.

Published
2017

44. Formal Verification of a Floating-Point Expansion Renormalization Algorithm

Author

Valentina Popescu, Sylvie Boldo, Jean-Michel Muller, Mioara Joldes, Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria), Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre National de la Recherche Scientifique (CNRS), Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Arithmetic and Computing (ARIC), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire de l'Informatique du Parallélisme (LIP), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Centre National de la Recherche Scientifique (CNRS), ANR-14-CE25-0018,Fast Relax,Approximation rapide et fiable(2014), Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon), Université de Lyon-École normale supérieure - Lyon (ENS Lyon)-Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Université Claude Bernard Lyon 1 (UCBL), École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), and Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL)

Subjects
Correctness, Floating point, floating-point expansions, floating-point arithmetic, [INFO.INFO-AO]Computer Science [cs]/Computer Arithmetic, Proof assistant, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 010103 numerical & computational mathematics, 02 engineering and technology, Mathematical proof, 01 natural sciences, Formal proof, 020202 computer hardware & architecture, Renormalization, formal proof, multiple-precision arithmetic, Arbitrary-precision arithmetic, 0202 electrical engineering, electronic engineering, information engineering, Coq, 0101 mathematics, Algorithm, Formal verification, Mathematics
Abstract

International audience; Many numerical problems require a higher computing precision than the one offered by standard floating-point formats. A common way of extending the precision is to use floating-point expansions. As the problems may be critical and as the algorithms used have very complex proofs (many sub-cases), a formal guarantee of correctness is a wish that can now be fulfilled, using interactive theorem proving. In this article we give a formal proof in Coq for one of the algorithms used as a basic brick when computing with floating-point expansions, the renormaliza-tion, which is usually applied after each operation. It is a critical step needed to ensure that the resulted expansion has the same property as the input one, and is more " compressed ". The formal proof uncovered several gaps in the pen-and-paper proof and gives the algorithm a very high level of guarantee.

Published
2017

45. Real and Numerical Analysis

Author

Sylvie Boldo and Guillaume Melquiond

Subjects
Scheme (programming language), Real analysis, Simple (abstract algebra), Computer science, Bounded function, Numerical analysis, Convergence (routing), Applied mathematics, Wave equation, computer, computer.programming_language
Abstract

For the vast majority of FP users, FP arithmetic is not a research topic per se. It is just a tool to quickly get a result, hopefully accurate. This chapter describes experiments that extend beyond the realm of simple FP arithmetic toward real analysis and numerical analysis. Our running example comes from numerical analysis: it is a program to get an approximation to the solution of the 1D wave equation described. This application requires mathematical theorems that would have been next to impossible to prove using the real analysis formalization from Coq’s standard library. This is why we use another formalization of real analysis detailed, in particular to prove the existence and regularity of the solution of the 1D wave equation using d’Alembert’s formula. The properties of the numerical scheme, e.g. convergence, are proved. Then the round-off errors are bounded. Finally, the verification of the C program is explained.

Published
2017

46. Compilation of FP Programs

Author

Guillaume Melquiond and Sylvie Boldo

Subjects
Software portability, Computer science, Programming language, Compiler, computer.software_genre, computer
Abstract

The IEEE-754 standard has improved the portability and reproducibility of the results of FP programs by mandating that every basic FP operation be performed as if the result was first computed with infinite precision and then rounded to the target format. In particular, most hardware components providing FP arithmetic are nowadays compliant with this standard. Unfortunately, this still does not guarantee that an FP program will behave in a reproducible way, as both the programming language and the compiler can interfere with the proper execution of FP arithmetic.

Published
2017

47. Numerical Software Verification

Author

Sylvie Boldo and Alessandro Abate

Subjects
Computer science, Numerical analysis, Computational science
Published
2017

48. The Coq System

Author

Guillaume Melquiond and Sylvie Boldo

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Software, Computer science, business.industry, Programming language, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Proof assistant, Logical rules, State (computer science), business, Mathematical proof, computer.software_genre, computer
Abstract

The Coq software is a proof assistant, that is, its primary purpose is to let users state theorems, to help them write the proofs of these theorems, and to finally check that these proofs are correct with respect to some logical rules. This chapter gives only the most basic concepts about Coq. It is not meant to replace the reference manual or some actual books on the topic.

Published
2017

49. Preface

Author

Sylvie Boldo and Guillaume Melquiond

Published
2017

50. Error-Free Computations and Applications

Author

Sylvie Boldo and Guillaume Melquiond

Subjects
Discrete mathematics, Transformation (function), Arithmetic underflow, Square root, Computation, Rounding, Multiplication, Division (mathematics), Operand, Mathematics
Abstract

Even if FP computations are inexact most of the time, we can prove the exactness of some computations or retain some exactness using remainders as done in this chapter. We are interested in subcases where an FP computation is error-free, and will give several sufficient assumptions. When an FP computation is not exact, we moreover aim at computing the error it made, using FP operators only. This kind of algorithm is called an error-free transformation (EFT). Given an operation ◇ on two operands x and y, the corresponding EFT produces two FP numbers r h and r l such that r h = □( x ◇ y ) and x ◇ y = r h + r l . In other words, the EFT produces the rounding of the operation and the exact error of this operation. These operators will probably be recommended by the next version of the IEEE-754 standard (that will be published in 2018) for the addition (denoted as augmentedAddition) and the multiplication (denoted by augmentedMultiplication). When the error cannot be represented by an FP number (as in the case of division and square root), we will study the conditions needed to ensure that the remainders x − □ x / y ⋅ y and x − □ x 2 are representable by an FP number. These remainders can then be used in subsequent computations. The algorithms for computing these EFTs are well-known and their formalization adds an extra level of guarantee. In particular, the requirements on the radix and the handling of underflow have to be specified.

Published
2017

Catalog

Books, media, physical & digital resources
See catalog results