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

- Algebras for Correctness of Sequential Computations (Isabelle theory uniformly describing preconditions, correctness statements and calculi for sequential computation models including monotonic Boolean transformers which need a theory with Lattice properties; as PDF)
- Algebras for Iteration and Infinite Computations (Isabelle theory describing iterations and computation models with aborting, finite and infinite executions)
- An Algebraic Approach to Computations with Progress (Isabelle theory describing algebras for computations with progress such as passing of time or traces getting longer; as PDF)
- An Algebraic Approach to Multirelations and their Properties (Isabelle theory describing algebras of multirelations; as PDF)
- An Algebraic Framework for Minimum Spanning Tree Problems (ZIP file with Isabelle2016-1 theories proving the correctness of Prim's minimum spanning tree algorithm based on algebras for aggregation; presented in four documents: Stone Algebras (PDF) and Stone Relation Algebras (PDF) and Stone-Kleene Relation Algebras (PDF) and An Algebraic Framework for Minimum Spanning Tree Problems (PDF))
- Closure, Properties and Closure Properties of Multirelations (Isabelle theory describing algebras of multirelations; as PDF)
- Infinite Executions of Lazy and Strict Computations (Isabelle theory uniformly describing infinite executions, recursion and iteration in strict and non-strict computation models; as PDF)
- Relation-Algebraic Verification of Prim's Minimum Spanning Tree Algorithm (ZIP file with Isabelle theories proving the correctness of Prim's minimum spanning tree algorithm; as PDF)
- Stone Relation Algebras (ZIP file with Isabelle2016 theories generalising relation algebras to the weighted-graph model; presented in three documents: Stone Algebras (link to AFP) and Stone Relation Algebras (PDF) and Stone-Kleene Relation Algebras (PDF))
- Unifying Correctness Statements (Isabelle theory uniformly describing preconditions, correctness statements and calculi for various sequential computation models; as PDF)
- Unifying Lazy and Strict Computations (Isabelle theory giving a unified semantics to recursion and iteration in strict and non-strict computation models; as PDF)
- A technical report with consolidated Isabelle theories from my research until 2015
- Isabelle repository for relational and algebraic methods (Georg Struth's page)

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