Toward mechanical verification of properties of roundoff error propagation

In this paper we will be concerned with portions of roundoff analysis which can be automated. Conditions are given under which proofs of numerical stability can be performed completely automatically and very economically (in particular, in polynomial time). We also discuss the use of "numerical heuristics" which apply "hill-climbing" methods to functionals measuring contamination from roundoff.