Char presents a qualitative method for certifying the numerical stability of multivariate floating point rational expressions when computations are done in standard fixed precision arithmetic. He points out that this method is not a replacement for alternative forms of stability analysis, although it can help discover the stability of rational expressions in a straightforward manner.

After specifying a model for floating point computation and the desired properties of operands, the author presents some of the rules of reasoning that form the basis for his method of stability analysis. The expression analyzer that implements this algorithm combines declarations of the known properties of the operands with the backward-chaining theorem proving method to test the stability of an input expression given in parse-tree form. An appendix illustrates the ease of use of this automatic analyzer. The paper contains little information on the behavior of the analyzer when it is unable to find a proof of stability. Following some discussion of improving this implementation, the paper looks at how this method can also be employed to do useful quantitative error bounding. The author assumes that the reader is knowledgeable about automatic theorem proving and computer arithmetic.