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.

My research is about computation models and their use to develop correct programs. I devise algebras to describe the meaning of programs and create proofs to show that programs are correct. The proofs are formally verified using automated theorem provers.

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

Isabelle Theories

I implement proofs in the theorem prover Isabelle. 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

Publications

  • ... all publications
  • Stone-Kleene Relation Algebras, AFP, 2017
  • Stone Relation Algebras, LNCS 10226:127-143, RAMiCS 2017
  • An Algebraic Approach to Multirelations and their Properties (with R. Berghammer), JLAMP 88:45-63, 2017
  • 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
    admin@cosc.canterbury.ac.nz
  • Computer Science and Software Engineering
    University of Canterbury
    Private Bag 4800, Christchurch
    New Zealand
  • Follow us
    FacebookYoutubetwitterLinked In