Department of Computer Science
Steve Reeves' Personal Web Page

I am currently a Professor in the Department of Computer Science at the University of Waikato.

Here is a Quicktime movie made from photos I took during the Summer School on Specification Languages in Slovakia in 2005.


  • In 2013 I am teaching:
  • In previous years I've taught: The last four courses were taught in my previous incarnations at QMW, University of London and at the University of Essex.

    Return to Index




    My research interests centre around ways of describing, in a high-level 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 summed-up 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 security-critical 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.


    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 'ISuRF-Improving 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 state-chart. 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 model-based 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 Martin-Lö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.


    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.

    Return to Index


    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 three-year stint I have now retired to a full-time teacher and researcher again :-).

    In the past I've also been Pro-Dean for the School of Computing and Mathematical Sciences and deputy CoD of Computer Science.

    Return to Index

    Post-graduate Research opportunities

    If you are interested by any of the work described here and would like to know more about post-graduate research in these areas then you can email me: my email name is stever and the place is

    Return to Index


    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 Addison-Wesley 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!

    Logic for Computer Science

    To see all my publications to date, go to the Department's publications page and look for my name amongst the authors.

    Return to Index

    Return to Index

    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 to get to me too
    Last updated: 28th March 2013