Marc Daumas
We present in this paper a library to compute with Taylor models, a technique extending interval arithmetic to reduce decorrelation and to solve differential equations. Numerical software usually produces only numerical results. Our library…
We provide a framework to bound the probability that accumulated errors were never above a given threshold on hybrid systems. Such systems are used for example to model an aircraft or a nuclear power plant on one side and its software on…
The ability to detect fragments of deleted image files and to reconstruct these image files from all available fragments on disk is a key activity in the field of digital forensics. Although reconstruction of image files from the file…
Formal proof checkers such as Coq are capable of validating proofs of correction of algorithms for finite field arithmetics but they require extensive training from potential users. The delayed solution of a triangular system over a finite…
Cody & Waite argument reduction technique works perfectly for reasonably large arguments but as the input grows there are no bit left to approximate the constant with enough accuracy. Under mild assumptions, we show that the result computed…
Real number calculations on elementary functions are remarkably difficult to handle in mechanical proofs. In this paper, we show how these calculations can be performed within a theorem prover or proof assistant in a convenient and highly…
Graphics Processing Units (GPUs) are now powerful and flexible systems adapted and used for other purposes than graphics calculations (General Purpose computation on GPU -- GPGPU). We present here a prototype to be integrated into…
Gappa uses interval arithmetic to certify bounds on mathematical expressions that involve rounded as well as exact operators. Gappa generates a theorem with its proof for each bound treated. The proof can be checked with a higher order…
This paper provides a bound on the number of numeric operations (fixed or floating point) that can safely be performed before accuracy is lost. This work has important implications for control systems with safety-critical software, as these…
Les unit\'{e}s graphiques (Graphic Processing Units- GPU) sont d\'{e}sormais des processeurs puissants et flexibles. Les derni\`{e}res g\'{e}n\'{e}rations de GPU contiennent des unit\'{e}s programmables de traitement des sommets (vertex…
Most existing implementations of multiple precision arithmetic demand that the user sets the precision {\em a priori}. Some libraries are said adaptable in the sense that they dynamically change the precision of each intermediate operation…