# 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):

- A Hierarchy of Algebras for Boolean Subsets (AFP entry describing structures with a subset that forms a Boolean algebra)
- An Algebraic Framework for Minimum Spanning Tree Problems (proving the correctness of Prim's minimum spanning tree algorithm based on algebras for aggregation; relevant AFP entries are Stone Algebras and Stone Relation Algebras and Stone-Kleene Relation Algebras and Aggregation Algebras and Relational Minimum Spanning Tree Algorithms)
- Relation-Algebraic Verification of Disjoint-Set Forests (AFP entry proving the total correctness of path halving, path splitting and union-by-rank)
- Relation-Algebraic Verification of Prim's Minimum Spanning Tree Algorithm (proving the correctness of Prim's minimum spanning tree algorithm; relevant AFP entries are Stone Algebras and Stone Relation Algebras and Stone-Kleene Relation Algebras and Aggregation Algebras and Relational Minimum Spanning Tree Algorithms)
- Relational Characterisations of Paths (AFP entry characterising different classes of paths and rooted paths and proving the correctness of basic algorithms)
- Second-Order Properties of Undirected Graphs (AFP entry specifying undirected acyclic graphs in relation algebras with a Kleene star)
- Stone Relation Algebras (generalising relation algebras to the weighted-graph model; relevant AFP entries are Stone Algebras and Stone Relation Algebras and Stone-Kleene Relation Algebras)
- Verifying Minimum Spanning Tree Algorithms with Stone Relation Algebras (proving the total correctness of Kruskal's minimum spanning tree algorithm; relevant AFP entries are Stone Algebras and Stone Relation Algebras and Stone-Kleene Relation Algebras and Aggregation Algebras and Relational Minimum Spanning Tree Algorithms)
- Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras (AFP entry proving the total correctness of union and find with path compression)

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
- 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