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, The Group is 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. The Group does not want to build software that usually works – it wants software that always works, and in the way intended by the requirements.

For more information visit the Formal Methods Laboratory.