Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
scientific article; zbMATH DE number 6761449