1Formal Correctness and Stability of Dense Linear Algebra Algorithms

derivation of algorithms for linear algebra operations. Rather than proving loop based algorithms correct a posteriori, a sys-tematic methodology is employed that determines loop invari-ants from a mathematical specification of a given linear alge-bra operation. Algorithms and their correctness proofs are then constructively derived from this loop invariant. The process has been made mechanical via a prototype sys-tem implemented with Mathematica. Once an algorithm has been determined, a similarly systematic a posteriori process is used to determine the correctness in the presence of roundoff error (stability properties) of the algorithm. In this paper, we report progress towards the ultimate goal of full automation of the system. Keywords—formal derivation, linear algebra algorithms, sta-bility analysis, automated system, mechanical derivation I