Verification and Numerical Algorithms
LMS Computer Science Colloquium
in association with the
EPSRC Network on Numerical Algorithms and High Performance Computing
Tuesday 13th November 2012
The aim of the colloquium is 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 will interest both Graduate Students and more established researchers undertaking work in these areas, and the event will provide an occasion for informal networking and the exploration of connections between Numerical Analysis and Formal Verification. All interested Mathematicians and Computer Scientists are warmly encouraged to participate in this unique colloquium.
To register, please contact Duncan Turton, sending a copy of the registration form.
The day is free for students and £5 for all others which is payable on the day. A sandwich lunch will be provided.
11.00-12.00: Jean-Michel Muller (ENS Lyon)
Proof of Properties in Floating-Point Arithmetic
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)
Formal verification of safety-critical software
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.
13.00 – 14.00: Lunch
14.00 – 15.00: Daniel Kroening (University of Oxford)
Deciding Floating-Point Logic with Systematic Abstraction
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)
Numerical Algorithms in Hardware
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.
16.00-16.30: Tea
Limited funds are available to help with students’ travel costs. Further details are available from Duncan Turton at the Society
Submitted by Donald Eastwood on
