WhyMP, a formally verified arbitrary-precision integer library

DOI10.1145/3373207.3404029MaRDI QIDQ5145995zbMATH OpenOpenAlexWikidataFDO

Authors Guillaume Melquiond, Raphaël Rieu-Helft

Publication date 22 January 2021

Published in Proceedings of the 45th International Symposium on Symbolic and Algebraic Computation (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-02566654v2/file/main.pdf

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Recommendations

• WhyMP, a formally verified arbitrary-precision integer library
• A Why3 proof of GMP algorithms
• How to get an efficient yet verified arbitrary-precision integer library
• A Why3 framework for reflection proofs and its application to GMP's algorithms
• Verifying branch-free assembly code in Why3

Cited in

(3)

• Motivations for an arbitrary precision interval arithmetic and the MPFI library
• WhyMP, a formally verified arbitrary-precision integer library
• WhyMP

Describes a project that uses

Uses Software

• HACL*
• Why3

This page was built for publication: WhyMP, a formally verified arbitrary-precision integer library

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145995)