Toccata

Formally Verified Programs, Certified Tools and Numerical Computations

• Accueil
• Membres
• Logiciels
  • Logiciels
  • Galerie de
    programmes vérifiés
• Projets
• Publications
• Postes

An Efficient Arbitrary-Precision Integer Library

An arbitrary-precision integer library in the style of GMP, designed to be both efficient and formally proved correct.

Auteurs: Raphaël Rieu-Helft

Catégories: Arithmetic / Pointer Programs / Proofs by reflection / Non-linear Arithmetic

Outils: Why3

see also the index (by topic, by tool, by reference, by year)

This library implements arbitrary-precision integers in the style of GMP. Supported operations are addition, multiplication, division, comparisons, shifts square root and modular exponentiation on non-negative integers, as well as some basic operations on relative integers.

More detailed information on the C library is available in the WhyMP repository, as well as in the papers:

• "How to Get an Efficient yet Verified Arbitrary-Precision Integer Library" by Raphaël Rieu-Helft, Claude Marché and Guillaume Melquiond, published in VSTTE'2017 proceedings, Springer LNCS.
• "A Why3 framework for reflection proofs and its application to GMP's algorithms" by Guillaume Melquiond and Raphaël Rieu-Helft, published in IJCAR'2018 proceedings, Springer LNAI.
• "Formal Verification of a State-of-the-Art Integer Square Root" by Guillaume Melquiond and Raphaël Rieu-Helft, published in ARITH'2019 proceedings.
• "A Why3 proof of GMP algorithms" by Raphaël Rieu-Helft, published in Journal of Formalized Reasoning, ASDD-AlmaDL, 2019.