arXiv subjects

Marc Daumas

Publications and source records attributed to Marc Daumas.

11 recordsLinked to original sources

arXiv2009

Stochastic Formal Methods for Hybrid Systems

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 other side. This report contains simple formulas based on Lévy's and Markov's inequalities and it presents a formal theory of random variables with a special focus on producing concrete results. We selected four very common applications that fit in our framework and cover the common practices of hybrid systems that evolve for a long time. We compute the number of bits that remain continuously significant in the first two applications with a probability of failure around one against a billion, where worst case analysis considers that no significant bit remains. We are using PVS as such formal tools force explicit statement of all hypotheses and prevent incorrect uses of theorems.

cs.MS↗

arXiv2009

Using Graphics Processors for Parallelizing Hash-based Data Carving

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 fragments on disk can be accomplished by simply comparing the content of sectors on disk with the content of known files, this brute-force approach can be time consuming. This paper presents results from research into the use of Graphics Processing Units (GPUs) in detecting specific image file byte patterns in disk clusters. Unique identifying pattern for each disk sector is compared against patterns in known images. A pattern match indicates the potential presence of an image and flags the disk sector for further in-depth examination to confirm the match. The GPU-based implementation outperforms the software implementation by a significant margin.

cs.DC↗

arXiv2008

Formal proof for delayed finite field arithmetic using floating point operators

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 field mixes operations on integers and operations on floating point numbers. We focus in this report on verifying proof obligations that state that no round off error occurred on any of the floating point operations. We use a tool named Gappa that can be learned in a matter of minutes to generate proofs related to floating point arithmetic and hide technicalities of formal proof checkers. We found that three facilities are missing from existing tools. The first one is the ability to use in Gappa new lemmas that cannot be easily expressed as rewriting rules. We coined the second one ``variable interchange'' as it would be required to validate loop interchanges. The third facility handles massive loop unrolling and argument instantiation by generating traces of execution for a large number of cases. We hope that these facilities may sometime in the future be integrated into mainstream code validation.

cs.SC↗

arXiv2007

Verified Real Number Calculations: A Library for Interval Arithmetic

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 automated as well as interactive way. First, we formally establish upper and lower bounds for elementary functions. Then, based on these bounds, we develop a rational interval arithmetic where real number calculations take place in an algebraic setting. In order to reduce the dependency effect of interval arithmetic, we integrate two techniques: interval splitting and taylor series expansions. This pragmatic approach has been developed, and formally verified, in a theorem prover. The formal development also includes a set of customizable strategies to automate proofs involving explicit calculations over real numbers. Our ultimate goal is to provide guaranteed proofs of numerical properties with minimal human theorem-prover interaction.

cs.MS↗

arXiv2007

Formally Verified Argument Reduction with a Fused-Multiply-Add

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 with a fused-multiply-add provides a fully accurate result for many possible values of the input with a constant almost accurate to the full working precision. We also present an algorithm for a fully accurate second reduction step to reach double full accuracy (all the significand bits of two numbers are significant) even in the worst cases of argument reduction. Our work recalls the common algorithms and presents proofs of correctness. All the proofs are formally verified using the Coq automatic proof checker.

cs.MS↗

arXiv2007

Certification of bounds on expressions involving rounded operators

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 logic automatic proof checker, either Coq or HOL Light, and we have developed a large companion library of verified facts for Coq dealing with the addition, multiplication, division, and square root, in fixed- and floating-point arithmetics. Gappa uses multiple-precision dyadic fractions for the endpoints of intervals and performs forward error analysis on rounded operators when necessary. When asked, Gappa reports the best bounds it is able to reach for a given expression in a given context. This feature is used to quickly obtain coarse bounds. It can also be used to identify where the set of facts and automatic techniques implemented in Gappa becomes insufficient. Gappa handles seamlessly additional properties expressed as interval properties or rewriting rules in order to establish more intricate bounds. Recent work showed that Gappa is perfectly suited to the proof of correctness of small pieces of software. Proof obligations can be written by designers, produced by third-party tools or obtained by overloading arithmetic operators.

cs.MS↗

arXiv2007

Graphic processors to speed-up simulations for the design of high performance solar receptors

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 simulation codes that estimate temperature, velocity and pressure to design next generations of solar receptors. Such codes will delegate to our contribution on GPUs the computation of heat transfers due to radiations. We use Monte-Carlo line-by-line ray-tracing through finite volumes. This means data-parallel arithmetic transformations on large data structures. Our prototype is inspired on the source code of GPUBench. Our performances on two recent graphics cards (Nvidia 7800GTX and ATI RX1800XL) show some speed-up higher than 400 compared to CPU implementations leaving most of CPU computing resources available. As there were some questions pending about the accuracy of the operators implemented in GPUs, we start this report with a survey and some contributed tests on the various floating point units available on GPUs.

cs.DC↗

arXiv2006

Stochastic Formal Methods: An application to accuracy of numeric software

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 systems are now running fast enough and long enough for their errors to impact on their functionality. Furthermore, worst-case analysis would blindly advise the replacement of existing systems that have been successfully running for years. We present here a set of formal theorems validated by the PVS proof assistant. These theorems will allow code analyzing tools to produce formal certificates of accurate behavior. For example, FAA regulations for aircraft require that the probability of an error be below $10^{-9}$ for a 10 hour flight.

cs.MS↗

arXiv2006

Caractéristiques arithmétiques des processeurs graphiques

Les unités graphiques (Graphic Processing Units- GPU) sont désormais des processeurs puissants et flexibles. Les dernières générations de GPU contiennent des unités programmables de traitement des sommets (vertex shader) et des pixels (pixel shader) supportant des opérations en virgule flottante sur 8, 16 ou 32 bits. La représentation flottante sur 32 bits correspond à la simple précision de la norme IEEE sur l'arithmétique en virgule flottante (IEEE-754). Les GPU sont bien adaptés aux applications avec un fort parallélisme de données. Cependant ils ne sont que peu utilisés en dehors des calculs graphiques (General Purpose computation on GPU -- GPGPU). Une des raisons de cet état de faits est la pauvreté des documentations techniques fournies par les fabricants (ATI et Nvidia), particulièrement en ce qui concerne l'implantation des différents opérateurs arithmétiques embarqués dans les différentes unités de traitement. Or ces informations sont essentielles pour estimer et contrôler les erreurs d'arrondi ou pour mettre en oeuvre des techniques de réduction ou de compensation afin de travailler en précision double, quadruple ou arbitrairement étendue. Nous proposons dans cet article un ensemble de programmes qui permettent de découvrir les caractéristiques principales des GPU en ce qui concerne l'arithmétique à virgule flottante. Nous donnons les résultats obtenus sur deux cartes graphiques récentes: la Nvidia 7800GTX et l'ATI RX1800XL.

cs.MS↗

arXiv2006

A library of Taylor models for PVS automatic proof checker

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 can be used to produce both results and proofs. As seen during the development of Fermat's last theorem reported by Aczel 1996, providing a proof is not sufficient. Our library provides a proof that has been thoroughly scrutinized by a trustworthy and tireless assistant. PVS is an automatic proof assistant that has been fairly developed and used and that has no internal connection with interval arithmetic or Taylor models. We built our library so that PVS validates each result as it is produced. As producing and validating a proof, is and will certainly remain a bigger task than just producing a numerical result our library will never be a replacement to imperative implementations of Taylor models such as Cosy Infinity. Our library should mainly be used to validate small to medium size results that are involved in safety or life critical applications.

cs.MS↗

arXiv2001

Computer validated proofs of a toolset for adaptable arithmetic

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 individually to deliver the target accuracy according to the actual inputs. We present in this text a new adaptable numeric core inspired both from floating point expansions and from on-line arithmetic. The numeric core is cut down to four tools. The tool that contains arithmetic operations is proved to be correct. The proofs have been formally checked by the Coq assistant. Developing the proofs, we have formally proved many results published in the literature and we have extended a few of them. This work may let users (i) develop application specific adaptable libraries based on the toolset and / or (ii) write new formal proofs based on the set of validated facts.

cs.MS↗