BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Case Study: Verifying an Efficient Algorithm to Compute Bernoulli 
 Numbers - Manuel Eberl (Universität Innsbruck)
DTSTART:20250612T104500Z
DTEND:20250612T114500Z
UID:TALK230644@talks.cam.ac.uk
DESCRIPTION:The Bernoulli numbers B(k) are a sequence of rational numbers 
 that is ubiquitous in mathematics\, but difficult to compute efficiently (
 compared to e.g. approximating &pi\;.\n&nbsp\;\nIn 2008\, Harvey gave the 
 currently fastest known practical way for computing them: his algorithm co
 mputes B(k) mod p in time O(p\nlog^(1+o(1)) p). By doing this for O(k) man
 y small primes p in parallel and then combining the results with the Chine
 se Remainder Theorem\, one recovers the value of B(k) as a rational number
  in O(k&sup2\; log^(2+o(1)) k) time. One advantage of this approach is tha
 t the expensive part of the algorithm is highly parallelisable and has ver
 y low memory requirements.\nThis algorithm still holds the world record wi
 th its computation of B(10^8).\n&nbsp\;\nWe give a fully verified efficien
 t LLVM implementation of this algorithm. This was achieved by formalising 
 the necessary mathematical background theory in Isabelle/HOL\, proving an 
 abstract version of the algorithm correct\, and refining this abstract ver
 sion down to LLVM using Lammich's Isabelle-LLVM framework\, including many
  low-level optimisations. The performance of the resulting LLVM code is co
 mparable with Harvey's original unverified and hand-optimised C++ implemen
 tation.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR