LMS Computer Science Day, Tuesday 13th November 2012
Verification and Numerical Algorithms
LMS Computer Science Colloquium
in association with the EPSRC Network on Numerical Algorithms and High Performance Computing, at the London Mathematical Society.
The aim of the colloquium was to provide an opportunity for dialogue between researchers working in the Mathematics of Numerical Algorithms and Computer Scientists working in Formal Verification of numerical programs. The programme of talks was aimed at both Graduate Students and more established researchers undertaking work in these areas, and the event provided an occasion for informal networking and the exploration of connections between Numerical Analysis and Formal Verification.
11.00-12.00: Jean-Michel Muller (ENS Lyon)
Floating-point (FP) arithmetic was originally designed as a mere approximation to real arithmetic. And yet, since the behaviour of each operation is fully specified by the IEEE-754 standard for floating-point arithmetic, FP arithmetic can also be viewed as a mathematical structure on which it is possible to design algorithms and proofs. We give some examples that show the interest of that point of view.
12.00-13.00: David Monniaux (CNRS/VERIMAG Grenoble)
Safety-critical software (e.g. fly-by-wire aircraft controls) poses special concerns; the development and quality insurance methods used in other contexts are not sufficient for the high level of reliability demanded. Formal methods address this need by considering a formal, mathematical model of the execution of programs, and proving theorems over this model (automatically or manually). Floating-point computations pose specific problems: not only is the mapping from high-level programming constructs to low-level floating-point computational instructions often ill-specified, but also research in formal methods had largely disregarded floating-point issues until the 2000s. This talk will discuss some of these problems and proposed solutions.
14.00 – 15.00: Daniel Kroening (University of Oxford)
We present a procedure for bit-precise reasoning about IEEE binary floating-point arithmetic. The core of our approach is a non-trivial generalisation of the conflict analysis algorithm used in modern SAT solvers to lattice-based abstractions. The result is a sound and complete procedure for floating-point arithmetic that outperforms the state-of-the-art significantly on problems that check ranges on numerical variables.
15.00-16.00: George A. Constantinides (Imperial College London)
Computer architecture is in a state of flux, resulting in a fundamental re-think of efficient hardware. In this context, research into using programmable hardware to implement computational structures is beginning to take on an urgent role as it helps to define future architectural innovation. Once the restrictions of existing architectures are lifted, immense possibilities open up for efficient implementation of numerical algorithms. What number representations to use? How to organise data storage to match the choice of parallel datapath? To what degree can architectures be customised to an application or a class of applications? How can these tasks be automated? With these possibilities emerge a variety of complex verification challenges. We will discuss some of these questions and illustrate the impact - present and potential - with some case studies from my research group.