2025/05/24 by David K. Zhang, Alex Aiken, Zhang, David K. +1 · 1 citation
Computer Science · Engineering · #FOS: Computer and information sciences #FOS: Mathematics #Fault Detection and Control Systems #Logic in Computer Science (cs.LO) #Numerical Analysis (math.NA) #Petri Nets in System Modeling
paper · pdf · doi:10.48550/arxiv.2505.18791
openalex publication_date 2025/05/24 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Floating-point accumulation networks (FPANs) are key building blocks used in many floating-point algorithms, including compensated summation and double-double arithmetic. FPANs are notoriously difficult to analyze, and algorithms using FPANs are often published without rigorous correctness proofs. In fact, on at least one occasion, a published error bound for a widely used FPAN was later found to be incorrect. In this paper, we present an automatic procedure that produces computer-verified proofs of several FPAN correctness properties, including error bounds that are tight to the nearest bit. Our approach is underpinned by a novel floating-point abstraction that models the sign, exponent, and number of leading and trailing zeros and ones in the mantissa of each number flowing through an FPAN. We also present a new FPAN for double-double addition that is faster and more accurate than the previous best known algorithm.