Formal Numerical Program Analysis

William M. Farmer, F. Javier Thayer

1994

Abstract

This paper describes a method for formally analyzing numerical
programs and a software system that implements the method.  The
software system translates a purely functional PreScheme program that
manipulates machine integers into a representation in the IMPS
Interactive Mathematical Proof System.  The correctness of the
PreScheme program is analyzed by stating and proving conjectures
about the IMPS representation using the IMPS theorem proving facility.