# Invited Talks at SMT 2014

## SMT: Where do we go from here?

*Clark Barrett, New York University*

There is no question that the last decade has been a remarkable success story
for SMT. Yet, many challenges remain that are obstacles to unlocking the full
potential of this technology. In this talk, I will take a look at what
has brought SMT to this point, including some notable success stories. Then I
will discuss some of the remaining challenges, both technical and
non-technical, and suggest directions for addressing these challenges.

##
Automating the verification of floating-point algorithms

*Guillaume Melquiond, Inria*

Floating-point numbers are limited both in range and in precision, yet
they are widely used as a way to implement computations on real numbers.
Thus arithmetic operations introduce small errors which might be
amplified during subsequent computations and cause inaccuracies. As
such, proving the correctness of a floating-point algorithm usually
entails verifying that the computed results are still close enough to
some ideal values, despite the method error and the round-off errors.
The traditional way to tackle such a verification is to perform an error
analysis, possibly using automated tools.

Unfortunately, when it comes to the low-level functions found in
mathematical libraries, the floating-point code is usually so contrived
that this approach falls short. Indeed, just knowing the code is no
longer sufficient to verify it, one also has to know the mathematical
reasons that led to choosing this code in the first place. This excludes
any hope of full automation, yet automated tools are sorely needed, if
only because performing a pen-and-paper proof of such functions is long,
tedious, and error-prone.

This talk will show some issues specific to the verification of the
floating-point functions of a mathematical library, and some methods for
solving them automatically. These methods will be exemplified using
Gappa, a tool dedicated to proving the logical formulas that arise
during the verification of small yet complicated floating-point
algorithms. This tool is based on interval arithmetic, expression
rewriting, and theorem saturation. For increased confidence, the tool
also generates formal proofs which can be verified by the Coq proof
assistant.