Formally verified certificate checkers for hardest-to-round computation

DOI10.1007/S10817-014-9312-2MaRDI QIDQ2352500zbMATH OpenOpenAlexFDO

Authors Érik Martin-Dorel, Micaela Mayero, Laurent Théry, Guillaume Hanrot

Publication date 2 July 2015

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-00919498/file/Hensel-JAR.pdf

zbMATH Keywords

certificate checkersformal proofsHensel's lemmamodular arithmetic

Mathematics Subject Classification ID

Error analysis and interval analysis (65G99) Specification and verification (program logics, model checking, etc.) (68Q60) Symbolic computation and algebraic computation (68W30)

Recommendations

• Floating-point arithmetic in the Coq system
• Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover
• Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
• Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system
• Verified compilation of floating-point computations

Cites work

• A Hensel lifting to replace factorization in list-decoding of algebraic-geometric and Reed-Solomon codes
• A refinement-based approach to computational algebra in Coq
• Algorithmic Number Theory
• An introduction to small scale reflection in Coq
• Automatic Data Refinement
• Canonical Big Operators
• Data refinement in Isabelle/HOL
• Factoring polynomials with rational coefficients
• Finding a small root of a bivariate integer equation; factoring with high bits known
• Finding a small root of a univariate modular equation
• Finding smooth integers in short intervals using CRT decoding
• First-Class Type Classes
• Handbook of Floating-Point Arithmetic
• scientific article; zbMATH DE number 1936673 (Why is no real title available?)
• scientific article; zbMATH DE number 2188983 (Why is no real title available?)
• Improved decoding of Reed-Solomon and algebraic-geometry codes
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• On the adjugate matrix
• Refinements for free!
• Searching worst cases of a one-variable function using lattice reduction
• Simplified High-Speed High-Distance List Decoding for Alternant Codes
• Small solutions to polynomial equations, and low exponent RSA vulnerabilities
• Types for Proofs and Programs

Cited in

(7)

• \(\mathcal H\)-OCSP: A protocol to reduce the processing burden in online certificate status validation
• A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
• Formally verified approximations of definite integrals
• The Proof Certifier Checkers
• Berlekamp Zassenhaus
• Formally verified roundoff errors using SMT-based certificates and subdivisions
• Formalizing Coppersmith's method in Isabelle/HOL

Describes a project that uses

Uses Software

• Autoref
• Coq
• Coq/SSReflect

This page was built for publication: Formally verified certificate checkers for hardest-to-round computation

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