profile picture

Heiko Becker

PhD Student

Language Skills
  • German: Native Speaker
  • English: Professional
  • French: Medium

About Me

I am a PhD student at MPI-SWS in the group for Automated Verification and Approximation lead by Eva Darulova. In general I have a strong interest in static analysis and compilers for finite-precision programs. For these tools my main focus is on establishing rigorous correctness proofs of their behaviours.

We are currently working on verified compilation of floating-point programs in the presence of optimizing compilers. So far we have designed a new semantics called Icing that is able to model floating-point optimizations in a verified compiler.

In a second project we worked on building a certification backend for my supervisors previous work in the Daisy framework. We have developed a checker for Daisy's results in both Coq and HOL4. The checker certifies correctness for a single run of the Daisy static analyzer.

Projects

Dandelion A verified certificate checker for polynomial approximations of elementary functions
RealCake (integrated into CakeML) A verified and optimizing compiler for floating-point arithmetic, implemented as an extension to CakeML
Icing A new, nondeterministic floating-point source semantics and a proof-of-concept connection to the CakeML verified compiler.
FloVer A verified certificate checker for finite-precision roundoff errors. FloVer is implemented in both Coq and HOL4 and the implementations can be found at our GitLab server .

Teaching

May 2019 - August 2019

Advised Nathaniel Bos during his DAAD-funded internship. The goal of the internship was to develop a natural language interface for proofs in the HOL4 interactive theorem prover.

March 2019 - April 2019

Teaching assistant for blockseminar on "Advanced Program Analysis"

Since September 2018

Co-advising Joachim Bard during his Masters at MPI-SWS.

March 2018 - November 2018

Co-advised Nikita Zyuzin during his Masters at MPI-SWS. The goal of the master thesis was to extend FloVer with a formalization of affine arithmetic and implement new certificate checking functions that use affine arithmetic to compute tighter bounds.

January 2017 - June 2017

Co-advised Raphael Monat during his internship at MPI-SWS. The goal of the internship was to extend FloVer with support for mixed-precision verification.

Summer Term 2017

Teaching assistant for Static Program Analysis course

Summer Term 2014, Summer Term 2013

Student assistant for lecture Programmierung 2

Education

January 2016 - December 2016

Preparatory Phase of the Graduate School of Computer Science at Saarland University

Summer Term 2015 - Winter Term 2015/2016

Master studies at Saarland University

Winter Term 2010/2011 - Winter Term 2014/2015

Bachelor studies, Bachelor thesis on Verified SMT-based Translation Validation. Supervised by Prof. Dr. Sebastian Hack and Sigurd Schneider

Publications

Dandelion: Certified Approximations of Elementary Functions (Under publication) Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, and Jean-Baptiste Jeannin;
Interactive Theorem Proving (ITP); 2022 Show abstract
Abstract close

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 in library functions typically provide only a limited set of precisions, and are too inefficient for many applications. Polynomial approximations that are customized to a limited input domain and output accuracy can provide superior performance. In fact, the Remez algorithm computes the best possible approximation for a given polynomial degree, but has so far not been formally verified. This paper presents Dandelion, an automated certificate checker for polynomial approximations of elementary functions computed with Remez-like algorithms that is fully verified in the HOL4 theorem prover. Dandelion checks whether the difference between a polynomial approximation and its target reference elementary function remains below a given error bound for all inputs in a given constraint. By extracting a verified binary with the CakeML compiler, Dandelion can validate certificates within a reasonable time, fully automating previous manually verified approximations.

Verified Compilation and Optimization of Floating-Point Programs in CakeML Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, and Anthony Fox;
European Conference on Object-Oriented Programming; 2022 Show abstract
Abstract close

Verified compilers such as CompCert and CakeML have become increasingly realistic over the last few years, but their support for floating-point arithmetic has thus far been limited. In particular, they lack the “fast-math-style” optimizations that unverified mainstream compilers perform. Supporting such optimizations in the setting of verified compilers is challenging because these optimizations, for the most part, do not preserve the IEEE-754 floating-point semantics. However, IEEE-754 floating-point numbers are finite approximations of the real numbers, and we argue that any compiler correctness result for fast-math optimizations should appeal to a real-valued semantics rather than the rigid IEEE-754 floating-point numbers. This paper presents RealCake, an extension of CakeML that achieves end-to-end correctness results for fast-math-style optimized compilation of floating-point arithmetic. This result is achieved by giving CakeML a flexible floating-point semantics and integrating an external proof-producing accuracy analysis. RealCake’s end-to-end theorems relate the I/O behavior of the original source program under real-number semantics to the observable I/O behavior of the compiler generated and fast-math-optimized machine code. The artifact is available at https://doi.org/10.4230/DARTS.8.2.10

Lassie: HOL4 Tactics by Example Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, and Rupak Majumdar;
Certified Programs and Proofs (CPP); 2021 Video Slides Show abstract
Abstract close

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 requirement that the domain expert is also an expert in the low-level details in constructing the proof in a theorem prover. In particular, the user needs to select a sequence of tactics that lead to a successful proof, a task that in general requires knowledge of the exact names of a large set of tactics.

We present Lassie, a tactic framework for the HOL4 theorem prover that allows individual users to define their own tactic language by example, and for instance give frequently used tactics or tactic combinations easier-to-remember names. The core of Lassie is an extensible semantic parser, which allows the user to interactively extend the tactic language through a process of definitional generalization. Defining tactics in Lassie thus does not require any knowledge in implementing custom tactics, while proofs written in Lassie retain the correctness guarantees provided by the HOL4 system. We show through case studies how Lassie can be used in small and larger proofs by novice and more experienced interactive theorem prover users, and how we envision it to ease the learning curve in a HOL4 tutorial.

Formally Verified Roundoff Errors using SMT-based Certificates and Subdivisions (Tool Paper) Joachim Bard, Heiko Becker, and Eva Darulova;
International Symposium on Formal Methods (FM); 2019 Video Slides Show abstract
Abstract close

When compared to idealized, real-valued arithmetic, finite precision arithmetic introduces unavoidable errors, for which numerous tools compute sound upper bounds. To ensure soundness, providing formal guarantees on these complex tools is highly valuable. In this paper we extend one such formally verified tool, FloVer. First, we extend FloVer with an SMT-based domain using results from an external SMT solver as an oracle. Second, we implement interval subdivision on top of the existing analyses. Our evaluation shows that these extensions allow FloVer to efficiently certify more precise bounds for nonlinear expressions.

Icing - Supporting Fast-math Style Optimizations in a Verified Compiler Heiko Becker, Eva Darulova, Magnus O. Myreen, and Zachary Tatlock;
Computer-Aided Verification (CAV); 2019 Slides Show abstract
Abstract close

Verified compilers like CompCert and CakeML offer increasingly sophisticated optimizations. However, their deterministic source semantics and strict IEEE 754 compliance prevent the verification of “fast-math” style floating-point optimizations. Developers often selectively use these optimizations in mainstream compilers like GCC and LLVM to improve the performance of computations over noisy inputs or for heuristics by allowing the compiler to perform intuitive but IEEE 754-unsound rewrites. We designed, formalized, implemented, and verified a compiler for Icing, a new language which supports selectively applying fast-math style optimizations in a verified compiler. Icing’s semantics provides the first formalization of fast-math in a verified compiler. We show how the Icing compiler can be connected to the existing verified CakeML compiler and verify the end-to-end translation by a sequence of refinement proofs from Icing to the translated CakeML. We evaluated Icing by incorporating several of GCC’s fast-math rewrites. While Icing targets CakeML’s source language, the techniques we developed are general and could also be incorporated in lower-level intermediate representations.

A Verified Certificate Checker for Finite-Precision Error Bounds Heiko Becker, Nikita Zyuzin, Raphael Monat, Eva Darulova, Magnus O. Myreen, and Anthony Fox;
Formal Methods in Computer-Aided Design (FMCAD); 2018 Slides Show abstract
Abstract close

Being able to soundly estimate roundoff errors in finite-precision computations is important for many applications in embedded systems and scientific computing. Due to the unintuitive nature of finite-precision arithmetic, automated static analysis tools are highly valuable for this task. The results, however, are only as correct as the implementations of the static analysis tools. This paper presents a formally verified and modular tool which fully automatically checks the correctness of finite-precision roundoff error bounds encoded in a certificate. We present implementations of certificate generation and checking for both Coq and HOL4 and evaluate it on a number of examples from the literature. The experiments use both in-logic evaluation of Coq and HOL4, and execution of extracted code outside of the logics. We benchmark Coq extracted unverified OCaml code and a CakeML-generated verified binary.

Combining Tools for Optimization and Analysis of Floating-Point Computations Heiko Becker, Pavel Pancheckha, Eva Darulova, and Zachary Tatlock;
International Symposium on Formal Methods (FM); 2018 Slides Show abstract
Abstract close

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, each focusing on a distinct aspect of numerical programming. Building reliable floating point applications typically requires addressing several of these aspects, which makes easy composition essential. This paper describes the composition of two recent floating-point tools; Herbie, which performs accuracy optimization, and Daisy, which performs accuracy verification. We find that the combination provides numerous benefits to users, such as being able to use Daisy to check whether Herbie’s unsound optimizations improved the worst-case roundoff error, as well as benefits to tool authors, including uncovering a number of bugs in both tools. The combination also allowed us to compare the different program rewriting techniques implemented by these tools for the first time. The paper lays out a road map for combining other floating-point tools and for surmounting common challenges.

Daisy-Framework for Analysis and Optimization of Numerical Programs (Tool Paper) Eva Darulova, Anastasiia Izycheva, Fariha Nasir, Fabian Ritter, Heiko Becker, and Robert Bastian;
International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS); 2018
A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms Heiko Becker, Jasmin Christian Blanchette,Uwe Waldmann and Daniel Wand;
CADE-26. LNCS, Springer; 2017
Comparing Repositories Visually with RepoGrams Daniel Rozenberg, Ivan Beschastnikh, Fabian Kosmale, Valerie Poser, Heiko Becker, Marc Palyart, Gail C. Murphy;
Proceedings of the 13th International Conference on Mining Software Repositories; 2016

Data Protection Imprint