
Here is a Quicktime movie made from photos I took during the Summer School on Specification Languages in Slovakia in 2005.
Supervision
Introduction
My research interests centre around ways of describing, in a highlevel and precise mathematical way, what a piece of software does and then using that description to form a basis for the development of that software  which is to say that I'm primarily interested in specification, program development and programming languages.
This is usually summedup by saying that I work in 'formal methods'  this is essentially that area of Computer Science which uses mathematical notations and ideas (like 'proof') for developing designs for software and then exploring their properties mathematically  just as civil and mechanical engineering have calculus, so software engineering has formal methods.
There's an excellent source of information on this at The Oxford Formal Methods archives .
One obvious practical reason to be interested in formal methods is that they give a way of designing trustable safety and securitycritical systems. These are systems in which we need to have the highest possible confidence. Formal methods are clearly a way of getting to this goal as far as software is concerned.
A good source of information in this area is The Oxford Safety Critical Systems archives .
We have a formal
methods lab at Waikato!
Developments in Formal Methods
Z is one of the most widely used formal specification languages and in a current project, started during Martin Henson's sabbaticals here in early 1997 and 2001 and during my sabbaticals at Essex in late 1997 and 2000 (and several shorter visits since then), we began work on a critique of Z and a reconstruction of it (originally based on intensional and constructive notions). There is a page that describes our work here.
Grants
I have held grants funded by the New Zealand government's Foundation for Research, Science and Technology (FRST) for the ten years since 1997, and you can find out more by looking at the FM group's web page.
Two of the grants funded by FRST were for a project called 'ISuRFImproving Software using Requirements Formalization', and the other grant funded a project which investigated the use of Z as a basis for program refinement, and as a basis for giving the semantics for a type of statechart. There is more information on both these projects (and others) on the formal methods lab page.
I currently have a BuildIT Fellowship which is held by Judy Bowen. We are working on formal modelling for "whole" systems, with an emphasis on the user interface. Form our models we can do things like derive tests (à la modelbased testing) and give plans for developing usability tests, which is especially valuable for, say, formal methods people who have little experience in that area.
Teaching Formal Methods
Another aspect of my research in the less recent past has been to consider ways of supporting the teaching of formal methods. Everything that is written about the need for tools to support formal methods applies even more to the art of teaching them. Having tools available not only teaches students about the tools themselves but also helps to stop the details of the formality from obscuring the fundamental ideas by relieving the students and teachers of a lot of the responsibility for taking care of those details.
Working in this area not only needs knowledge of formal methods and tools to support them, but also experience in teaching formal methods and experience in producing systems to support teaching. See the page on MiraCalc for an example of work completed a while ago on supporting the teaching of functional programming and logic for an example from this area.
Another piece of software that I've developed (based on the work of Alan Hamilton of Stirling University in Scotland) is called PICTCalc. This is a proof assistant for working in MartinLöf's Constructive Type Theory. CTT is, essentially, a single language within which we can both specify and implement programs  so, instead of having to use, say Z, to specify and then another language, say Haskell or C++, to implement the specification in, the whole enterprise takes place within one language.
CTT is a very elegant formal embodiment of the ideas behind intuitionistic
logic  this differs from the usual 'classical' logic that we see in courses
like 140 in that, most famously, sentences like A \/ ¬ A are not valid,
i.e. not true in every possible valuation. This seems strange at first,
but it turns out to be just the sort of logic we need for describing computations.
Conclusions
Within New Zealand work in the each of the areas I've mentioned above is still not very common  which means that there is great potential for new projects  a small interest group whose aim is to provide a focus for such work has been established  read about The New Zealand Formal Program Development Colloquium for details, though it has only met informally for the past few years.
I am currently Associate Dean, Software Engineering in the School of Computing and Mathematical Sciences.
I was Chairperson of the Department of Computer Science from 2003 to 2006, and after my threeyear stint I have now retired to a fulltime teacher and researcher again :).
In the past I've also been ProDean for the School of Computing and Mathematical Sciences and deputy CoD of Computer Science.
Postgraduate Research opportunities
If you are interested by any of the work described here and would like to know more about postgraduate research in these areas then you can email me: my email name is stever and the place is @cs.waikato.ac.nz.
The logic textbook "Logic for Computer Science" that I wrote with Mike Clarke (many years ago) is now available for free. It went out of publication with AddisonWesley and they were not interested in a new edition. However, I regularly have requests for copies, so I did some work on the (Word!!!) source from 1990, and produced PDF and Postscript versions which you can download. I'd be interested to hear comments!
To see all my publications to date, go to the Department's publications page and look for my name amongst the authors.
Return to my official home page
Return to The Department of Computer Science Home Page
Steve Reeves, email name stever and you'll have to add @cs.waikato.ac.nz to get to me too
Last updated: 28th March 2013