New paper related to GMP library

[Nelson H. F. Beebe]

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: beebe at math.utah.edu  -
- 155 S 1400 E RM 233                       beebe at acm.org  beebe at computer.org -
- Salt Lake City, UT 84112-0090, USA    URL: http://www.math.utah.edu/~beebe/ -
-------------------------------------------------------------------------------