WhyMP, a formally verified arbitrary-precision integer library

DOI10.1016/j.jsc.2022.07.007OpenAlexW4289779274MaRDI QIDQ2673999

Guillaume Melquiond, Raphaël Rieu-Helft

Publication date: 22 September 2022

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jsc.2022.07.007

zbMATH Keywords

mathematical libraryinteger arithmeticdeductive program verification

Mathematics Subject Classification ID

Artificial intelligence (68Txx) Theory of computing (68Qxx) Theory of software (68Nxx)

Related Items (1)

WhyMP

Uses Software

• gmp
• Isabelle/HOL
• Why3
• WhyML
• HACL*

Cites Work

• Unnamed Item
• Unnamed Item
• The spirit of ghost code
• Verifying branch-free assembly code in Why3
• How to get an efficient yet verified arbitrary-precision integer library
• A Why3 framework for reflection proofs and its application to GMP's algorithms
• A proof of GMP square root
• One Logic to Use Them All
• WhyMP, a formally verified arbitrary-precision integer library
• Improved Division by Invariant Integers
• Why3 — Where Programs Meet Provers
• Logic for Programming, Artificial Intelligence, and Reasoning

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