Enabling Pivoting in the Formal Derivation of LU factorization

2023/04/06 by Robert A. Geijn, Myers, Margaret E., van de Geijn, Robert +4
Computer Science · Engineering · #FOS: Computer and information sciences #Formal Methods in Verification #G.4 #Mathematical Software (cs.MS) #Scheduling and Optimization Algorithms #VLSI and Analog Circuit Testing

paper · pdf · doi:10.48550/arxiv.2304.03068

openalex publication_date 2023/04/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

The FLAME methodology for deriving linear algebra algorithms from specification, first introduced around 2000, has been successfully applied to a broad cross section of operations. An open question has been whether it can yield algorithms for the best-known operation in linear algebra, LU factorization with partial pivoting (Gaussian elimination with row swapping). This paper shows that it can and provides general techniques for pivoted factorizations.

Related

• LU factorization with panel rank revealing pivoting and its communication avoiding version
• Gaussian Elimination with Randomized Complete Pivoting
• A Reexamination of the COnfLUX 2.5D LU Factorization Algorithm
• A New Upper Bound For the Growth Factor in Gaussian Elimination with Complete Pivoting
• Matrix Factorizations with Uniformly Random Pivoting