A Why3 proof of GMP algorithms
From MaRDI portal
Publication:5130751
DOI10.6092/ISSN.1972-5787/9730zbMATH Open1451.68342MaRDI QIDQ5130751FDOQ5130751
Authors: Raphaël Rieu-Helft 
Publication date: 28 October 2020
Recommendations
Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Certification of bounds on expressions involving rounded operators
- Why3 -- where programs meet provers
- Title not available (Why is that?)
- Title not available (Why is that?)
- An axiomatic basis for computer programming
- One logic to use them all
- Integer and polynomial multiplication: towards optimal Toom-Cook matrices
- A proof of GMP square root
- The spirit of ghost code
- Logic for Programming, Artificial Intelligence, and Reasoning
- 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
- Improved Division by Invariant Integers
Cited In (5)
- WhyMP, a formally verified arbitrary-precision integer library
- Formally verified Montgomery multiplication
- 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 Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
Uses Software
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)
