Colloquium Details
Using Theorem Proving in Industry
| Author: | John Harrison Intel Corporation |
|---|---|
| Date: | June 07, 2001 |
| Time: | 15:30 |
| Location: | 220 Deschutes |
Abstract
In this talk we'll give an outline of our work applying the HOL Light theorem prover to some applications at Intel connected with floating-point arithmetic, e.g. the formal verification of division, square root and transcendental function algorithms. We'll give examples to illustrate the theorem prover features that seem particularly important for this kind of work, such as:
- Arithmetic decision procedures
- Programmability
- Pre-proved mathematics
Finally, we'll give some general comments about the potential for using theorem provers more widely in industry.