Ecole Normale Superieure de Lyon, Lyon, France
Wednesday 15 November - Thursday 16 November 2000


A two-day workshop on Certified Arithmetics was held on November 15-16 at Ecole Normale Superieure de Lyon. The workshop was intended to bring together researchers interested in mechanically proving properties of arithmetic operators and algorithms.


Wednesday 15 November


11:00 Welcome

11:30 Invited Talk: John Harrison (Intel): Formal Verification of Floating Point Algorithms

12:30 Lunch


14:00 Jean Michel Muller (Ens Lyon): A Few Things about Floating-Point Arithmetic (ppt)

14:30 Tom Kelsey (St. Andrews): Computer algebra and automated reasoning at St. Andrews

15:00 Invited Talk: Brigitte Verdonk (Anvers): On the development of a reliable integrated computational environment (pdf)

16:00 Coffee break

16:30 Deepak Kapur (New Mexico): Tables and Arithmetic Circuits: Content-based Reasoning

17:00 Guillaume Hanrot (INRIA): MPFR: A Library for Multiprecision Floating-point Arithmetic with Exact Rounding

17:30 Paul Zimmermann (INRIA): Square Root Proof with Coq

Thursday 16 November


09:00 Invited Talk: Mark Sofroniou (Wolfram Research): Precise Numerical Computation

10:00 Alberto Ciaffaglione (Udine): Co-Inductive Approach to Real Numbers

10:30 Coffe Break

11:00 David Russinoff (AMD): Floating-Point Verification with ACL2

11:30 Vincent Lefèvre (INRIA): The Table Maker's Dilemma

12:00 Laurent Théry (INRIA): Floating-Point Expansions in Coq

12:30 Lunch


14:00 Invited Talk: Johnathan Shewchuk (Berkeley): Expansion-Based Extended Precision Arithmetic

15:00 Francisco Palomo Lozano (Cadiz): Reasoning about Matrix Arithmetic in ACL2

15:30 Christian Jacobi (Saarbrucken): Proving the correctness of a complete floating point unit on the gate level

16:00 Coffee break

16:30 Discussion


An ACL2 Library of Floating Point Arithmetic

A Co-inductive Approach To Real Numbers (in Coq)

Coq: a library for floating point arithmetic

The MPFR library

Table Maker's Dilemma: worst case search

Computer Architecture (Saarbrucken)


The workshop was organized by the AOC Cooperative Action regrouping 3 INRIA research teams: Arénaire: (contact Jean-Michel Muller), Lemme (contact Loic Pottier) and Polka (contact Paul Zimmermann).


Laurent Thery
Last modified: Thu Dec 14 22:12:48 MET 2000