WhyMP, a formally verified arbitrary-precision integer library. (March 2023)

• Record Type: Journal Article
• Authors: Melquiond, Guillaume; Rieu-Helft, Raphaël
• Is Part Of: Journal of symbolic computation. Volume 115(2023)
• Page Start: 74
• Page End: 95
• Publication Date: 2023-03
• Subjects: Integer arithmetic -- Deductive program verification -- Mathematical library; Mathematics -- Data processing -- Periodicals; Numerical analysis -- Data processing -- Periodicals; Automatic programming (Computer science) -- Periodicals; Mathématiques -- Informatique -- Périodiques; Analyse numérique -- Informatique -- Périodiques; Programmation automatique -- Périodiques; Automatic programming (Computer science); Mathematics -- Data processing; Numerical analysis -- Data processing; Periodicals; Electronic journals; 510.285
• DOI: 10.1016/j.jsc.2022.07.007
• Languages: English
• ISSNs: 0747-7171

Abstract

Abstract: Arbitrary-precision integer libraries such as GMP are a critical building block of computer algebra systems. GMP provides state-of-the-art algorithms that are intricate enough to justify formal verification. In this paper, we present a C library that has been formally verified using the Why3 verification platform in about four person-years. This verification deals not only with safety, but with full functional correctness. It has been performed using a mixture of mechanically checked handwritten proofs and automated theorem proving. We have implemented and verified a nontrivial subset of GMP's algorithms, including their optimizations and intricacies. Our library provides the same interface as GMP and is almost as efficient for smaller inputs. We detail our verification methodology and the algorithms we have implemented, and include some benchmarks to compare our library with GMP.