Formal Methods Group

Established in 1998, this is the first Formal Methods laboratory in New Zealand. The work that goes on in this lab is based on the view that programming is at the heart of computer science. It is also based on the view that, as engineers and scientists, we should use the machinery of mathematics to model and reason about the systems that we build before we build them. This is in contrast with the view that programs should be written by trial and error (usually at great expense and with a high likelihood of failure, judged by current experience) with our users ironing out our mistakes for us at their expense. To this end, we are developing languages and tools for modelling systems, for reasoning about those models and for transforming them into code in a way that is guaranteed to preserve meaning and correctness. We do not want to build software that usually works – we want software that always works, and in the way intended by the requirements.

One particular project is aimed at producing methods that will allow the development of user-interfaces to the same level of dependability as the functional part of a system. We are also developing tools for generating test suites from specifications, to improve the cost-effectiveness of testing. We are investigating languages and logics for dealing with refinement at a general level, and techniques for developing discrete event systems.

Driving the work of the lab are problems that we have been presented with by various parts of the New Zealand (and beyond) software development industry. This means that we can be sure our work is going to be useful for solving problems that are important to people outside the research environment.

Further details on the group can be found at www.cs.waikato.ac.nz/research/fm/