SWS   Info

Public Audience

English

60 Minutes

Saarbrücken

Real-number arithmetic is a key component in many domains like neural
networks and embedded controllers, thus providing efficient and correct
tooling is highly desirable. As real numbers are infinite, they are
commonly represented using finite-precision arithmetic which makes
computations efficient but this representation necessarily introduces
errors into results. In safety-critical settings finite-precision programs
must thus come with rigorous proofs about their behavior, and it is the
compilers job to preserve these properties.

In general, compiler verification deals with exactly this task, proving
that the compiler preserves properties of the input program throughout the
compilation pipeline. As of today, the most-common formats of
floating-point and fixed-point numbers are not well supported by
state-of-the-art verified compilers.

In my thesis I want to improve the state-of-the-art support for
finite-precision arithmetic for verified compilation of numerical kernels
for floating-point and fixed-point arithmetic. For floating-point
arithmetic, state-of-the-art verified compilers, support only simple
direct mappings into assembly instructions.

In the thesis we develop a novel floating-point semantics that allows
verified compilers to perform performance oriented optimizations of
floating-point programs, and use this semantics to extend the verified
compiler CakeML with support for real-number programs. Fixed-point
arithmetic is not supported by major verified compilers.

For the remaining research work of the thesis, we suggest first an
approach to for verified code generation for fixed-point arithmetic. As an
alternative, we suggest an extension of a verified compiler with support
for fixed-point arithmetic.

--email hidden

Zoom

public