Leverhulme Lecture - Building Symbiotic Relationships Between Formal Verification and High Performance Computing

Robert Kirby

(University of Utah)

Computational simulations for scientific and engineering applications are becoming more ubiquitous as part of the engineering design cycle. The application of simulation science to complex problems often requires complex models, sophisticated numerics and intricate implementations. Tremendous effort has been expended towards the development of systematic techniques for model validation and numerical method verification. As most researchers hesitantly admit, the amount of time spent debugging intricate high performance parallel implementations of their simulations consumes a large bulk of their time. In particular, many would argue that although this debugging time is necessarily, it distracts one from the science or engineering problem of interest. In this talk, we will present our continuing effort by the Utah Gauss Group to employ formal verification techniques to the debugging of parallel high performance computing codes using MPI. This synergistic combination of formal techniques with HPC is designed to infuse news ways of thinking about parallel code design through interaction of two normally disparate communities, with the goal of benefiting both communities.
Tuesday 26th May 2009, 14:00
Robert Recorde Room
Department of Computer Science