I just recorded this new paper related to GMP: @String{j-J-SYMBOLIC-COMP = "Journal of Symbolic Computation"}
@Article{Melquiond:2023:WFV, author = "Guillaume Melquiond and Rapha{\"e}l Rieu-Helft", title = "{WhyMP}, a formally verified arbitrary-precision integer library", journal = j-J-SYMBOLIC-COMP, volume = "115", number = "??", pages = "74--95", month = mar # "\slash " # apr, year = "2023", CODEN = "JSYCEH", DOI = "https://doi.org/10.1016/j.jsc.2022.07.007", ISSN = "0747-7171 (print), 1095-855X (electronic)", ISSN-L = "0747-7171", bibdate = "Sat Sep 17 06:23:51 MDT 2022", bibsource = "http://www.math.utah.edu/pub/tex/bib/fparith.bib; http://www.math.utah.edu/pub/tex/bib/gnu.bib; http://www.math.utah.edu/pub/tex/bib/jsymcomp.bib", URL = "http://www.sciencedirect.com/science/article/pii/S0747717122000657", 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.", acknowledgement = ack-nhfb, fjournal = "Journal of Symbolic Computation", journal-URL = "http://www.sciencedirect.com/science/journal/07477171", keywords = "Deductive program verification; Integer arithmetic; Mathematical library", } ------------------------------------------------------------------------------- - Nelson H. F. Beebe Tel: +1 801 581 5254 - - University of Utah - - Department of Mathematics, 110 LCB Internet e-mail: be...@math.utah.edu - - 155 S 1400 E RM 233 be...@acm.org be...@computer.org - - Salt Lake City, UT 84112-0090, USA URL: http://www.math.utah.edu/~beebe/ - ------------------------------------------------------------------------------- _______________________________________________ gmp-devel mailing list gmp-devel@gmplib.org https://gmplib.org/mailman/listinfo/gmp-devel