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, with a strong focus on verification.

We are currently working on building a certification backend for her previous work in the Daisy framework. To this end we implement a checker for Daisy's results in both Coq and HOL4. The overall goal for our project is to support certification of analysis results computed by Daisy.

Projects

FloVer A verified certificate checker for floating-point roundoff errors.

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

Teaching

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

Publications

A Verified Certificate Checker for Floating-Point Error Bounds (under publication) Heiko Becker, Nikita Zyuzin, Raphael Monat, Eva Darulova, Magnus O. Myreen, and Anthony Fox;
Formal Methods in Computer-Aided Design (FMCAD); 2018 Show abstract
Abstractclose

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 Show abstract
Abstractclose

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 Verified Certificate Checker for Floating-Point Error Bounds Heiko Becker, Eva Darulova and Magnus O. Myreen;
ArXiv e-print; 2017 Show abstract
Abstractclose

Being able to soundly estimate roundoff errors in floating-point computations is important for many applications in embedded systems and scientific computing. Due to the unintuitive nature of floating-point arithmetic, automated static analysis tools are highly valuable for this task.

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