2nd Meeting on Testing and Verification for Computational Science
ucam kent epsrc ssi

The need for more rigorous software verification in computational science is well known. Often the responsibility is placed on the scientist, but increased care and attention is not enough. There is a wealth of research in computer science aimed at automating testing and verification, yet little of this has crossed over into practice in the sciences.

This meeting provides a forum to discuss recent work and new ideas, and to foster links between researchers interested in the intersection of verification, programming languages, and computational science. The meeting is aimed at both computer scientists and natural/physical scientists employing computational techniques.

Program

There will be coffee, tea and biscuits in FW26 starting from 1:15 pm for a 1:30 pm start.

TimeEventSpeakerTitle
1:15 pmArrive
1:30 pmKeynoteKonrad Hinsen The long road from ideas to bits and back: a traveller's guide to verifiable computational research
2:30 pmTalk Dan Liew Fun with Floats: Symbolic execution of floating point programs
2:55 pmBreak
3:10 pmTalk Luke Abraham How to do virtually everything with the Met Office Unified Model
3:35 pmTalk Alessandro Abate Sound and Automated Synthesis of Digital Controllers for Continuous Plants
4:00 pmTalk Ben Hall Pathological behaviours of single progenitor model defy inference techniques
4:25 pmBreak
4:40 pmTalk Wadud Miah Verification of Fortran Codes
5:05 pmTalk Mistral Contrastin Verifying spatial properties of stencil computations
5:30 pmLightning Talk Jonathan Pelham Using JupyterHub and PySpark to explore large datasets for errors
5:35 pmLightning Talk Girish Nivarti Direct Simulations of Turbulent Flames
5:40 pmLightning Talk Paul Hovland ProVESA: The Program Verification for Extreme-Scale Applications Project
5:45 pmClose
7:00 pmDrinks & Dinner at Queens' College

Logistics

William Gates Building

The Computer Laboratory is situated at 15 JJ Thomson Ave (CB3 0FD) on the West Cambridge site (map) and is easy to access via public transport.

Please contact us if you have any questions.

The meeting will be held in room FW26 (click for map) which is on the first floor to the right of the stairs on the west side of the building. We will post signage on the day, but you can enter at reception and ask to be directed.

For those looking for lunch first, there is a cafe directly below the meeting room, as well as other options on the West Cambridge campus.

Attending

Registration is free & anyone is welcome to attend the talks. The dinner reservations have now been set up at Queens' College for those who signed up prior to 17th March. Apologies, but we cannot increase the number of seats for dinner any further at this point in time.

Abstracts

We are very pleased to have Konrad Hinsen from the Centre de Biophysique Moléculaire, Orléans, France and Synchrotron SOLEIL, Saint Aubin, France giving our keynote this year:

Konrad Hinsen The long road from ideas to bits and back: a traveller's guide to verifiable computational research

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?

Dan Liew Fun with Floats: Symbolic execution of floating point programs

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.

Luke Abraham How to do virtually everything with the Met Office Unified Model

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.

Alessandro Abate Sound and Automated Synthesis of Digital Controllers for Continuous Plants

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.

Vicky Kostiou Pathological behaviours of single progenitor model defy inference techniques

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.

Wadud Miah Verification of Fortran Codes

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.

Mistral Contrastin Verifying spatial properties of stencil computations

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.


The meeting is part of the EPSRC project CamFort: Automated evolution and verification of computational science models at the Computer Laboratory.

Last modified: 2017-03-09 13:46:00 UTC