Projet ANR EVA-Flo : 4ème réunion, 22-23 septembre 2009, Lyon

Marc Daumas : 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 or 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 invariants by generating properties on arrays for a large number of cases. We hope that these facilities may sometime in the future be integrated into mainstream code validation.

Arnault Ioualalen : Compilation de programmes SCADE avec garantie de la précision numérique
La précision numérique est un domaine majeur pour les industries critiques comme l'aérospatiale ou l'aéronautique, sa finalité étant de garantir que les calculs qui sont effectués dans de tels systèmes soient corrects. Cet exposé a pour but de présenter les travaux effectués en ce sens pour le cadre des programmes décrits avec le logiciel SCADE, en utilisant les résultats de l'interprétation abstraite, ainsi qu'un nouveau modèle de représentation et d'équivalence de programmes présenté par R.Tate, M.Stepp, Z.Tatlock et S.Lerner. Notre approche concerne les problèmes de ré-écriture de programmes et d'équivalence sémantique entre ceux-ci, et les problèmes de mesure de la déviation du calcul. En outre notre outil s'apparente à un compilateur qui rend un programme sémantiquement équivalent mais dont l'erreur de calcul induite est bornée.

Andy Novocin: Gradual Sub-Lattice Reduction*
One of the primary uses of lattice reduction algorithms is to approximate short vectors in a lattice. I present a new algorithm which produces approximations of short vectors in certain lattices. It does this by generating a reduced basis of a sub-lattice which is guaranteed to contain all short vectors in the given lattice or as a proof that no short vectors exist. This algorithm has a complexity which is less dependent on the size of the input basis vectors and more dependent on the size of the output vectors. With unfavorable parameters the algorithm reduces the input basis completely with roughly the same complexity as floating-point LLL but with an alternative switch path.
To illustrate the usefulness of the new algorithm I will show how it can be used to give new complexity bounds for factoring polynomials in Z[x] and reconstructing algebraic numbers from approximations.

Retour à la page d'EVA-Flo.