How to get an efficient yet verified arbitrary-precision integer library

DOI10.1007/978-3-319-72308-2_6MaRDI QIDQ1630031zbMATH OpenOpenAlexFDO

Authors Raphaël Rieu-Helft, Claude Marché, Guillaume Melquiond

Publication date 7 December 2018

Full work available at URL https://hal.inria.fr/hal-01519732

zbMATH Keywords

C languagearbitrary-precision arithmeticdeductive program verificationWhy3 program verifier

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Recommendations

• A Why3 proof of GMP algorithms
• Verifying branch-free assembly code in Why3
• A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
• scientific article; zbMATH DE number 1670746
• Design of a parallel linear algebra library for verified computation

Cited in

(5)

• Motivations for an arbitrary precision interval arithmetic and the MPFI library
• WhyMP, a formally verified arbitrary-precision integer library
• A Why3 proof of GMP algorithms
• A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
• Verified runtime assertion checking for memory properties

Describes a project that uses

Uses Software

• Why3

This page was built for publication: How to get an efficient yet verified arbitrary-precision integer library

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