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 recent publications; some have been published in the Archive of Formal Proofs (AFP):

In earlier work I have developed algebras to describe iteration, infinite executions and correctness of sequential computations. Relevant Isabelle theories are available in a consolidated AFP entry and as part of AFP entries Stone Relation Algebras and Stone-Kleene Relation Algebras. They cover:

  • Algebras for Correctness of Sequential Computations (uniformly describing preconditions, correctness statements and calculi for sequential computation models)
  • Algebras for Iteration and Infinite Computations (describing iterations and computation models with aborting, finite and infinite executions)
  • An Algebraic Approach to Computations with Progress (describing algebras for computations with progress such as passing of time or traces getting longer)
  • An Algebraic Approach to Multirelations and their Properties (describing algebras of multirelations)
  • Closure, Properties and Closure Properties of Multirelations (describing algebras of multirelations)
  • Infinite Executions of Lazy and Strict Computations (uniformly describing infinite executions, recursion and iteration in strict and non-strict computation models)
  • Unifying Correctness Statements (uniformly describing preconditions, correctness statements and calculi for various sequential computation models)
  • Unifying Lazy and Strict Computations (giving a unified semantics to recursion and iteration in strict and non-strict computation models)

See also Georg Struth's Isabelle repository for relational and algebraic methods.

Research Grants

  • Algebras for reasoning about weighted graphs and graph algorithms
    JSPS Invitation Fellowship for Research in Japan, 2019
  • 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
  • Modal Algebra of multirelations (with H. Furusawa, G. Struth), JLC, published online 2024
  • An example of a goal-directed, calculational proof (with R. C. Backhouse, M. Winter), JFP 34:e13, 2024
  • Relation-Algebraic Verification of Disjoint-Set Forests, Fundamenta Informaticae 192(1):77-120, 2024
  • Determinism of multirelations (with H. Furusawa, G. Struth), JLAMP 139:100976, 2024
  • Cardinality and Representation of Stone Relation Algebras, AFP, 2023
  • Inner structure, determinism and modal algebra of multirelations (with G. Struth), AFP, 2023
  • Dependences between Domain Constructions in Heterogeneous Relation Algebras, RAMiCS 2023
  • Relation-algebraic verification of Borůvka's minimum spanning tree algorithm (with N. Robinson-O'Brien), LNCS 13027:225-240, RAMiCS 2021
  • Second-order properties of undirected graphs, LNCS 13027:209-224, RAMiCS 2021
  • Algebras for iteration, infinite executions and correctness of sequential computations, AFP, 2021
  • Relational Forests, AFP, 2021
  • Relational Minimum Spanning Tree Algorithms (with N. Robinson-O'Brien), AFP, 2020
  • Relational Characterisations of Paths (with R. Berghammer, H. Furusawa, P. Höfner), JLAMP 117:100590, 2020
  • Relational Disjoint-Set Forests, AFP, 2020
  • Relational Characterisations of Paths (with P. Höfner), AFP, 2020
  • Reasoning about Algebraic Structures with Implicit Carriers in Isabelle/HOL, LNCS 12167:251-268, IJCAR 2020
  • A Hierarchy of Algebras for Boolean Subsets (with B. Möller), LNCS 12062:152-168, RAMiCS 2020
  • Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras, LNCS 12062:134-151, RAMiCS 2020
  • A Hierarchy of Algebras for Boolean Subsets (with B. Möller), AFP, 2020
  • Connecting Fixpoints of Computations with Strict Progress, LNCS 11185:62-79, UTP 2019
  • Verifying Minimum Spanning Tree Algorithms with Stone Relation Algebras, JLAMP 101:132-150, 2018
  • An Algebraic Framework for Minimum Spanning Tree Problems, TCS 744:37-55, 2018
  • Aggregation Algebras, AFP, 2018
  • 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 369 2777
    Fax: +64 3 364 2569
    CSSEadministration@canterbury.ac.nz
  • Computer Science and Software Engineering
    University of Canterbury
    Private Bag 4800, Christchurch
    New Zealand
  • Follow us
    FacebookYoutubetwitterLinked In