Verifying an efficient algorithm for computing Bernoulli numbers

DOI10.4230/LIPICS.ITP.2025.35MaRDI QIDQ7323695zbMATH OpenFDO

Authors Manuel Eberl, Peter Lammich

Publication date 1 September 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2025.35

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper)
• A multimodular algorithm for computing Bernoulli numbers
• An extension of the table of Bernoulli numbers.
• Applying data refinement for monadic programs to Hopcroft's algorithm
• Computation of Tangent, Euler, and Bernoulli Numbers
• Fast and verified UNSAT certificate checking
• Fast computation of Bernoulli, tangent and secant numbers
• Formally verified Montgomery multiplication
• scientific article; zbMATH DE number 1557041 (Why is no real title available?)
• scientific article; zbMATH DE number 7649971 (Why is no real title available?)
• Modern computer algebra
• Modular Multiplication Without Trial Division
• Multiple zeta values at non-positive integers
• Number Theory
• On the calculation of Bernoulli's numbers up to \(B_{62}\) by means of Staudt's theorem.
• Refinement of parallel algorithms down to LLVM: applied to practically efficient parallel sorting

This page was built for publication: Verifying an efficient algorithm for computing Bernoulli numbers

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