Mechanical Derivation and Systematic Analysis of Correct Linear Algebra Algorithms

We consider the problem of developing formally correct dense linear algebra libraries. The problem would be solved convincingly if, starting from the mathematical specification of a target operation, it were possible to generate, implement and analyze a family of correct algorithms that compute the operation. This thesis presents evidence that for a class of dense linear operations, systematic and mechanical development of algorithms is within reach. It describes and demonstrates an approach for deriving and implementing, systematically and even mechanically, proven correct algorithms. It also introduces a systematic procedure to analyze, in a modular fashion, numerical properties of the generated algorithms