Meeting on Testing and Verification for Computational Science
              

Venue: Computer Laboratory, University of Cambridge

Date: Tuesday, March 15th 2016

Contact: Dominic Orchard or Andrew Rice.

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 will provide 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 scientists employing computational techniques.

The meeting will last the afternoon at the Computer Laboratory, University of Cambridge, followed by dinner at Queens' College. The meeting is part of the EPSRC project CamFort: Automated evolution and verification of computational science models at the Computer Laboratory.

Provisional schedule

12:30Introduction
    Dominic Orchard
12:45Keynote: From mathematics to programs, a verification journey  (slides)
    Sylvie Boldo
13:45Development and Verification of a Formal Model of Cell Transformation in Cancer  (slides)
    David Shorthouse
14:10Coffee
 
14:30Data-driven and model-based quantitative verification of complex systems  (slides)
    Alessandro Abate
14:55Linear Temporal Logic for Biologists in BMA
    Benjamin Hall
15:20What run-time services could help scientific programming?  (slides)
    Stephen Kell
15:45Can we verify/maintain a program if we can't do the maths?  (slides)
    James Davenport
16:10Coffee
 
16:30Testing Stochastic Models using Pseudo-Oracles
    Matthew Patrick
16:55Verification in Practice, Half a Century On  (slides)
    Nick Maclaren
17:20Testing and reviewing code for the Met Office Unified Model  (slides)
    Luke Abraham
17:45Validation and testing of High Performance Computing scientific community codes, is there light at the end of the tunnel?  (slides)
    Filippo Spiga
18:00Close
 
19:00Drinks reception at Queens' College (Old Senior Combination Room)
19:30Dinner at Queens' College

Keynote

We are thrilled to have Sylvie Boldo from Inria in Orsay, France giving the keynote:

From mathematics to programs: a verification journey

From a (partial) differential equation to an actual program is a long road. This talk will present the formal verification of all the steps. This includes the mathematical error due to the numerical scheme (method error), that is usually bounded by pen-and-paper proofs. This also includes round-off errors due to the floating-point computations. The running example will be a C program that implements a numerical scheme for the resolution of the one-dimensional acoustic wave equation. This program is annotated to specify both method error and round-off error, and formally verified using interactive and automatic provers.

Register

To register for attendance, please e-mail dominic.orchard@cl.cam.ac.uk. We officially closed registration on March 4th, but we may be able to accomodate a few more people for the meeting, so please e-mail if you are interested.

Registration is free and for those wishing to attend the dinner at Queens' College in the evening please registed by March 4th. There are 30 free places which will be allocated on a first-come-first-served basis, after which the cost will be roughly £38 a head (TBC). Please mention any dietary requirements in your registration e-mail.

Logistics

The Computer Laboratory is situated on the west side of Cambridge (map) and is most easily accessed from the Cambridge train station by taking a taxi or the Uni 4 bus. Cambridge is easily accessible by train from London King Cross. 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.

We will finish at 6pm, with a drinks reception at Queens' from 7pm and dinner starting at 7:30pm. We will head en-masse to Queens' after the end of the meeting. I will also provide directions on the day for those wishing to catch us up.


Last modified: 2016-07-19 09:08:49.043895 UTC