Computational Modelling Group

Seminar  22nd November 2016 2 p.m.  177/2023

Lightweight verification for computational science models

Dominic Orchard
School of Computing, University of Kent

Categories
NGCM, Scientific Computing, Software Engineering
Submitter
Hans Fangohr

Programming now plays a key role in science, both in data analysis as well as the construction of complex models. Therefore, verifying the correctness of our programs (i.e., that they do what we intended them to do) is ever more important. In this talk, I'll outline a verification technique called "lightweight specifications". A lightweight specification provides comments in code that describe certain aspects of a program. An automatic tool then checks conformance of the code against these specifications. I'll give two examples of lightweight specifications for numerical Fortran code: units-of-measure types, which specify the physical units of numerical quantities in a program; and stencil specifications which describe the pattern of data access used in array computations. Not only can we automatically verify that a program correctly implements these requirements but specifications provide documentation for future developers. Specifications can also be inferred and generated automatically in some cases, reducing programmer effort. I'll identify other related tools in different languages and finish by discussing future potential specification techniques for scientific code.

Bio:

Dominic is a lecturer at the School of Computing, University of Kent and a member of the Programming Languages and Systems group. Dominic has a PhD in Computer Science from the University of Cambridge and worked as a Research Associate at Imperial College London and the University of Cambridge before joining Kent. He is a fellow of the Software Sustainability Institute. Dominic is a big fan of functional programming and does research in the applications of programming language research to computational science and the interaction between semantics, logic, and types.