A Why3 proof of GMP algorithms
From MaRDI portal
Publication:5130751
Recommendations
Cites work
- scientific article; zbMATH DE number 3574936 (Why is no real title available?)
- scientific article; zbMATH DE number 1178976 (Why is no real title available?)
- A Why3 framework for reflection proofs and its application to GMP's algorithms
- A proof of GMP square root
- An axiomatic basis for computer programming
- Certification of bounds on expressions involving rounded operators
- How to get an efficient yet verified arbitrary-precision integer library
- Improved Division by Invariant Integers
- Integer and polynomial multiplication: towards optimal Toom-Cook matrices
- Logic for Programming, Artificial Intelligence, and Reasoning
- One logic to use them all
- The spirit of ghost code
- Verifying branch-free assembly code in Why3
- Why3 -- where programs meet provers
Cited in
(5)- Formally verified Montgomery multiplication
- How to get an efficient yet verified arbitrary-precision integer library
- WhyMP, a formally verified arbitrary-precision integer library
- A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
- A Why3 framework for reflection proofs and its application to GMP's algorithms
This page was built for publication: A Why3 proof of GMP algorithms
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5130751)
