WORKSHOP AOC
Ecole Normale Superieure de Lyon, Lyon, France
Wednesday 15 November - Thursday 16 November 2000
http://www-sop.inria.fr/lemme/AOC/workshop.html
TOPICS
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.
PROGRAM
Wednesday 15 November
Morning
- 11:00 Welcome
- 11:30 Invited Talk: John Harrison (Intel): Formal Verification of Floating Point Algorithms
- 12:30 Lunch
Afternoon
- 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
Morning
- 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
Afternoon
- 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
RELATED LINKS
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)
ORGANIZATION
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).