Polynomial Function Enclosures and Floating Point Software Verification

Mr Jan Duracz
Computer Science, Aston University

Proving partial correctness of floating point programs is a hard verification problem. This is in part because error analysis of finite precision computation is difficult and in part due to the high complexity of the generated verification conditions. Typical verification conditions that arise in this context are predicates with real inequalities as atoms and therefore numerical constraint solvers seem a natural choice for the automation of such proofs.

In the talk I will outline our use function enclosures as the numerical type to base a dedicated solver on. We present a prototype implementation and evaluate it on verification conditions arising from a simple, yet nontrivial program for which we present a functional correctness analysis.

If time permits I will also present a novel subdivision direction selection algorithm that harnesses some of the rich information carried by the function enclosures.