The translation of a scientific question into bit patterns in a computer's memory involves many steps, as does the back-translation of the results of a computation into scientific insight. Each step is a potential source of mistakes, and thus requires some form of verification before we can trust its correctness. In this talk, I will outline appropriate verification approaches for each step, which range from purely human efforts, in particular the critical inspection of formulas and program source code, to fully mechanical procedures such as type or unit checking. I will also adopt a long-term perspective, focussing on the tools, procedures, and teaching curricula that we ought to develop in order to establish a trustworthy verification chain for computational science, even if they require a change of habits compared to today's state of the art. In particular, I will argue for the necessity to develop digital scientific notations as the main human-computer interface of computer-aided research.

In the course of this discussion, I will also try to shed some light on a few long-standing mysteries in computational science: Why is testing floating-point code so difficult? Why is it so hard to make scientific computations reproducible? Why is there less use of static type checking in science, despite it being considered evidently beneficial in computer science? Why do we trust computations uncritically, even though we witness the unreliability of computing technology in daily life?

Manually reasoning about programs using floating point can be difficult. In this talk I'll walk through some examples of seemingly correct code and show how a program analysis technique called symbolic execution can be used to expose correctness problems.

The Met Office Unified Model (MetUM) is a state of the art general circulation model that has many different scientific settings. Ensuring that the code is well tested is essential, as it is used operationally worldwide, e.g. for weather & air-quality forecasts.

With over 900,000 lines of code and over 200 active developers on four continents, a comprehensive test harness is in place at the Met Office and partner sites to aid in development. However, what is available for UK academics and their groups, who wish to contribute to MetUM development, but do not have access to these resources?

This talk will discuss the recent developments made by the Met Office in running the MetUM in a virtual machine environment. I will cover using this environment for testing and training, and will give examples of the problems encountered, along with some solutions.

Modern control is implemented with digital microcontrollers, embedded within a dynamical plant that represents physical components. I present a new algorithm based on counter-example guided inductive synthesis that automates the design of digital controllers that are correct by construction. The synthesis result is sound with respect to the complete range of approximations, including time discretization, quantization effects, and finite-precision arithmetic and its rounding errors. The new algorithm is implemented in a toolbox and tested.

The development of cancer is a multistep process, driven the sequential acquisition of genomic alterations that transform cellular phenotype. The quantification of the effects of genetic and epigenetic on cellular dynamics is essential to understand the early stages in cancer evolution. A simple stochastic model captures the behaviour of stem cells in squamous epithelia in lineage tracing experiments. Here we discuss fundamental limitations of experimental analysis using this model arising from intrinsic properties of the model, and their implications for future studies of transformed stem cells.

Fortran is a popular language for computational science codes which typically run on large supercomputers. With the advent of large Petascale machines, there is a strong emphasis on parallel scalability and energy efficiency. However, knowledge of verification of Fortran codes is lacking and there is anecdotal evidence to suggest that there is an over-reliance compilers to verify codes. This presentation will introduce a simple verification workflow and present the NAG compiler and verification tools for Fortran codes.

Stencil computation is a ubiquitous programming idiom in scientific computing. It involves iterated assignments to an array from some combination of the values in the neighbourhood of the current indices of an iteration e.g. a[i][j] = a[i][j+1] + a[i][j-1] in a nested loop with i and j as induction variables. These are heavily used in scientific simulations as well as image processing algorithms.

The indexing behaviour may easily involve more than 10 terms indexing in two or three dimensions. This opens room for errors in offsets. We hypothesised that vast majority of stencil computations involve continuous and symmetrical offsets from induction variables. We present a succinct specification language that allows verifying such spatial properties.