Project topics and materials
Get Complete Project Material File(s) Now! »
Proving Numerical Properties
The need to estimate the computation errors due to the use of oatingpoint numbers is crucial in order to interpret how signicant the returned results are. Rounding-o errors or over ows may cause a serious loss of precision leading to an unexpected behavior of the software. Although scientists and engineers are aware of these intrinsic issues [Gol91, Ste74] and despite the fact that there exists a norm which claries and normalizes the hardware implementation of oating-point arithmetic [IEE85, IEE08], it is hard to tell, given an implementation of an algorithm, if the numerical
computations are safe, even for small programs.
Whenever, a loss of precision is detected, it is also interesting to point out the sources of this loss as a helpful feedback for the developer. Indeed, a minor local loss of precision may cause a wrong interpretation of a test, and hence lead to a wrong decision.
To make things clear, we consider the case of solving an ordinary dierential equation (ODE) using a computer. The solution could be approximated numerically using for instance the Euler method. The Euler method gives a numerical approximation to the ideal solution of the ODE which can not be computed explicitly. The method error is dened by the difference between the Euler approximation and the ideal solution. Now, the Euler approximation is implemented as a computer program. This program uses nite-precision numbers (typically oating-point numbers) for all intern
computations instead of real numbers, which introduces in turn what is called the computation error, or round-o error.
Although, the method errors could be theoretically estimated (with respect to the real numbers semantics), the computation errors are hard to estimate in general. The use of nite-precision numbers makes the estimation even harder. We give hereafter an overview of the known approaches used to estimate the computation errors.
Explicit Relational Abstract Domains
The polyhedra abstract domain [CH78] catches and propagates explicit linear relations between variables such that b1x1 + b2x2 , where x and y are two numerical variables and , , and are real numbers. The internal abstract object has two dual representations: an external representation and an internal representation. external representation: a polyhedron is dened as the intersection of a nite set of ane subspaces of Rp, where p is the number of numerical variables abstracted. Each ane subspace is in fact represented by hx; ii i. Equalities, hx; ii = i, are represented by two inequalities, hx; ii i and hx;ii i. A polyhedron is then by denition a convex subset of Rp.
Implicit Relational Abstract Domains
Ane arithmetic has been successfully used in many elds from the selfvalidation of numerical algorithms [CS93] where it was rstly introduced, to reliable computing to come up with tight enclosing intervals [Kol01, Kol04, Miy00, MK04a], and algebraic surface plotting [SLMW06]. In what follows, we motivate the use of ane forms by the dependency problems observed in both interval arithmetic, and an extension of IA, called generalized intervals.
Combining Abstract Domains
The direct product of two or more abstract domains is equivalent to performing the analysis separately with each abstract domain. This approach does not combine the expressiveness power of the abstract domains in use, and hence does not improve the nal result.
We brie y recall hereafter two dierent generic approaches designed to improve the precision of the analysis by sharing the information found by one domain in order to improve the result given by the other domain. The exchange of information is done dynamically during the analysis. Theoretically, these interleaves are strictly more expressive than each domain taken alone (as in direct product), nevertheless, in practice these approaches are either limited theoretically or need an extra eort to handle the exchange of information.
Table of contents :
Contents
1 Introduction
2 Context and Motivations
2.1 Proving Numerical Properties
2.2 Abstract Interpretation
2.3 Fluctuat
2.4 The ATV Case Study
3 Numerical Abstract Domains
3.1 Non Relational Abstract Domain
3.2 Explicit Relational Abstract Domains
3.3 Implicit Relational Abstract Domains
3.4 Combining Abstract Domains
4 Constrained Ane Sets
4.1 Introduction
4.2 Constrained Ane Sets
4.3 Special Case: Non Relational Constraints
5 Assignment and Interpretation of Tests
5.1 Abstract Assignment
5.2 Interpretation of Tests
5.3 Related Work
6 Join over Constrained Ane Sets
6.1 General Procedure
6.2 Join over Constrained Ane Forms
6.3 Join over Constrained Ane Sets
7 Implementation and Experiments
7.1 Abstract Computations Using Floating-point Numbers
7.2 Implementation
7.3 Experiments
8 Conclusion
A The Support Function
B Lengthy Proofs
B.1 Lemma 6.2.18: Fenchel Conjugate of L
B.2 Theorem 6.2.20: Saddle-Point Characterization
Bibliography
