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.