4 papers
Dandelion: Certified Approximations of Elementary Functions
Heiko Becker, Mohit Tekriwal, Eva Darulova +2
Elementary function operations such as sin and exp cannot in general be computed exactly on today's digital computers, and thus have to be approximated. The standard approximations…
Lassie: HOL4 Tactics by Example
Heiko Becker, Nathaniel Bos, Ivan Gavran +2
Proof engineering efforts using interactive theorem proving have yielded several impressive projects in software systems and mathematics. A key obstacle to such efforts is the requ…
Combining Tools for Optimization and Analysis of Floating-Point Computations
Heiko Becker, Pavel Pancheckha, Eva Darulova +1
Recent renewed interest in optimizing and analyzing floating-point programs has lead to a diverse array of new tools for numerical programs. These tools are often complementary, ea…
A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4
Heiko Becker, Nikita Zyuzin, Raphael Monat +3
Being able to soundly estimate roundoff errors of finite-precision computations is important for many applications in embedded systems and scientific computing. Due to the discrepa…