Parametric Floating-Point Reasoning

Because of their pervasive use in safety-critical applications and their potentially surprising semantics, the verification of floating-point algorithms is an important challenge.

For instance, Intel has been using interactive theorem proving to verify floating-point algorithms since 1994, when it lost $475 M because of an error in the floating-point division instruction of early Pentium processors.Interactive proof assistants support floating-point numbers whose bit size is unknown and given as a symbolic parameter.

Reasoning about floating-point numbers of symbolic size allows one to overcome fundamental limitations of fixed-size reasoning; it is crucial to develop reusable formal models of floating-point arithmetic.This project will enable modern SMT solvers to reason about floating-point numbers of symbolic size.

In radical departure from existing work, we will develop a reasoning technique that has built-in knowledge of floating-point arithmetic to achieve unprecedented automation for size-independent floating-point reasoning.This automation will be made available to users of interactive proof assistants. These employ a special software architecture to minimize the impact of bugs.

However, this architecture causes the efficient implementation of proof procedures to be more challenging.

This project aims to answer how trustworthy reasoning for floating-point numbers of symbolic size can be automated so that it scales to difficult conjectures and large proofs.