Walter Guttmann - Academic Staff - People - Computer Science and Software Engineering - University of Canterbury - New Zealand

Walter Guttmann

Algebra of computing

Please see the main page for contact, research and teaching information.

In this research I devise algebraic descriptions of computation models for sequential systems. A particular aim is to structure and unify the diversity of models described in the literature. To this end, I give axioms for key aspects of the models, for example, the infinite executions of a computation.

  • Some axioms are common to many models and frequently suffice to derive complex results, for example, program transformations and refinement rules for program development.
  • Individual models are characterised by adding specific axioms to the common ones, so that the resulting theories and methods specialise in various ways useful for different application areas.

According to the assumed axioms, the models are organised in a hierarchy of algebraic structures, the algebras of computing.

The theories are described by first-order axioms and ideally suited for support by automated theorem provers and SMT solvers. I implement them in Isabelle based on algebraic theories developed jointly with Georg Struth (Sheffield) and Tjark Weber (Uppsala). Our joint work applies the theory to perform automated reasoning about computing systems.

In recent work I am applying algebraic methods to verify the correctness of graph algorithms.

The following Isabelle theories are the basis of my most recent publications:

Research grants

  • Algebras of multirelations for modelling interaction and cooperation
    JSPS Invitation Fellowship for Research in Japan, 2015
  • General correctness: algebraic foundations and mechanisation
    DAAD Postdoc fellowship as visiting researcher at the University of Sheffield, 2010-2011


  • ... all publications
  • Stone Relation Algebras, RAMiCS 2017, to appear
  • An Algebraic Approach to Multirelations and their Properties (with R. Berghammer), JLAMP, to appear
  • Stone Relation Algebras, AFP, 2017
  • Relation-algebraic verification of Prim's minimum spanning tree algorithm, LNCS 9965:51-68, ICTAC 2016
  • Stone Algebras, AFP, 2016
  • An Algebraic Approach to Computations with Progress, JLAMP 85(4):520-539, 2016
  • Kleene Algebras with Domain (with V. B. F. Gomes, P. Höfner, G. Struth, T. Weber), AFP, 2016
  • Closure, Properties and Closure Properties of Multirelations (with R. Berghammer), LNCS 9348:67-83, RAMiCS 2015
  • A Relation-Algebraic Approach to Multirelations and Predicate Transformers (with R. Berghammer), LNCS 9129:50-70, MPC 2015
  • Infinite executions of lazy and strict computations, JLAMP 84(3):326-340, 2015
  • Algebras for Correctness of Sequential Computations, SCP 85(B):224-240, 2014
  • Extended Conscriptions Algebraically, LNCS 8428:139-156, RAMiCS 2014
  • Multirelations with Infinite Computations, JLAMP 83(2):194-211, 2014
  • Extended Designs Algebraically, SCP 78(11):2064-2085, 2013
  • Unifying Lazy and Strict Computations, LNCS 7560:17-32, RAMiCS 2012
  • Algebras for Iteration and Infinite Computations, Acta Informatica 49(5):343-359, 2012
  • Typing Theorems of Omega Algebra, JLAP 81(6):643-659, 2012
  • Unifying Correctness Statements, LNCS 7342:198-219, MPC 2012
  • Automating Algebraic Methods in Isabelle (with G. Struth, T. Weber), LNCS 6991:617-632, ICFEM 2011
  • Fixpoints for General Correctness, JLAP 80(6):248-265, 2011
  • A Repository for Tarski-Kleene Algebras (with G. Struth, T. Weber), CEUR-WS 760:30-39, ATE 2011
  • Towards a Typed Omega Algebra, LNCS 6663:196-211, RAMiCS 2011
  • Unifying Recursion in Partial, Total and General Correctness, LNCS 6445:207-225, UTP 2010
  • Partial, Total and General Correctness, LNCS 6120:157-177, MPC 2010
  • General Correctness Algebra, LNCS 5827:150-165, RelMiCS/AKA 2009
  • Phone: +64 3 364 2362
    Fax: +64 3 364 2569
  • Computer Science and Software Engineering
    University of Canterbury
    Private Bag 4800, Christchurch
    New Zealand
  • Follow us
    FacebookYoutubetwitterLinked In