Waikato Formal Methods Group
Explore the work of the Waikato Formal Methods Group and their innovative approaches.
Since 1998, our Formal Methods lab has been at the forefront of computer science in New Zealand. We believe that programming is a core aspect of computer science and that rigorous mathematical modelling is essential for building reliable software.
Instead of relying on trial and error, which can be costly and time-consuming, we focus on developing languages and tools that allow us to precisely model and reason about systems before they're built. Our goal is to create software that consistently works as intended, free from errors and bugs.
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.
What we do
- Write precise specifications and supporting logics to remove ambiguity early.
- Prove properties about systems and critical algorithms.
- Generate tests from specs to catch defects sooner.
- Provide evidence (proof logs, coverage, traceability) that supports audits and procurement.
Profiles
Professor
ORCID: 0000‑0002‑3840‑6060
Associate Dean Academic, Associate Professor
ORCID: 0000‑0003‑2815‑8267
Teaching Fellow
Teaching Fellow
Senior Lecturer, Programme Lead Software Engineering
Site/outputs: jessicadturner.github.io
Masters Student
Tom Levy
Lean 4 tooling, property‑based testing from specs.
Projects
Reeves, Levy
Goal: Make the specification the single source of truth.
What we’re building: a Lean 4 workflow where one spec produces conformance tests, a verified reference implementation, and CI evidence (proof logs, coverage, traceability). This extends the group’s long‑standing focus on test generation from specifications and dependable UI/UX artefacts.
Jaidka, Reeves, Bowen
Modelling and analysis of safety‑critical interactive devices using Coloured Petri Nets with Z‑based reasoning; case studies reported at APSEC/EICS/FM venues.
Bowen, Reeves
Methods and tools that bring user‑centred design together with formal specification and refinement to produce dependable interfaces as well as correct functionality.
Design and evaluation of decentralised technology that supports Māori communities to govern taonga and narratives (Ngā taonga o nehe rā me te heke mai).
Bowen; collaborations
Research on real‑time monitoring and participatory data design for worker safety and ethics in data use (e.g., forestry environments).
How we work
- Open tools and artefacts. We release code, examples, and documentation when possible.
- Plain language outputs. Alongside papers and proofs, we publish usage guides and CI recipes.
- Collaboration. We partner with researchers, industry, and public sector teams on practical case studies.
Get involved
- Students: MSc and PhD topics (Lean 4 tactics, test generation, evidence automation; HCI + FM).
- Collaborators: Joint case studies and co‑supervision welcome.
Contact
If you are a student or researcher interested in formal methods, contact us about current projects and supervision.