# Walter Guttmann

## Publications

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

### Edited books

- Relational and Algebraic Methods in Computer Science, RAMiCS 2018

### Journal articles

- Relational Characterisations of Paths (with R. Berghammer, H. Furusawa, P. Höfner),
**JLAMP**117:100590, 2020 - 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 - An algebraic approach to multirelations and their properties (with R. Berghammer),
**JLAMP**88:45-63, 2017 - A framework for automating security analysis of the Internet of Things (with M. Ge, J. B. Hong, D. S. Kim),
**JNCA**83:12-27, 2017 - An Algebraic Approach to Computations with Progress,
**JLAMP**85(4):520-539, 2016 - 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 - Multirelations with Infinite Computations,
**JLAMP**83(2):194-211, 2014 - Extended Designs Algebraically,
**SCP**78(11):2064-2085, 2013 - Algebras for Iteration and Infinite Computations,
**Acta Informatica**49(5):343-359, 2012 - Typing Theorems of Omega Algebra,
**JLAP**81(6):643-659, 2012 - Fixpoints for General Correctness,
**JLAP**80(6):248-265, 2011 - Imperative Abstractions for Functional Actions,
**JLAP**79(8):768-793, 2010 - Normal Design Algebra (with B. Möller),
**JLAP**79(2):144-173, 2010 - Tool Support for the Interactive Derivation of Formally Correct Functional Programs (with H. Partsch, W. Schulte, T. Vullinghs),
**J.UCS**9(2):173-188, 2003

### Conference papers

- 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), RAMiCS 2021
- Second-order properties of undirected graphs, RAMiCS 2021
- Reasoning about Algebraic Structures with Implicit Carriers in Isabelle/HOL, IJCAR 2020
- A Hierarchy of Algebras for Boolean Subsets (with B. Möller), RAMiCS 2020
- Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras, RAMiCS 2020
- Connecting Fixpoints of Computations with Strict Progress, UTP 2019
- Stone relation algebras, RAMiCS 2017
- Relation-algebraic verification of Prim's minimum spanning tree algorithm, ICTAC 2016
- Closure, Properties and Closure Properties of Multirelations (with R. Berghammer), RAMiCS 2015
- A Relation-Algebraic Approach to Multirelations and Predicate Transformers (with R. Berghammer), MPC 2015
- Extended Conscriptions Algebraically, RAMiCS 2014
- Unifying Lazy and Strict Computations, RAMiCS 2012
- Unifying Correctness Statements, MPC 2012
- Automating Algebraic Methods in Isabelle (with G. Struth, T. Weber), ICFEM 2011
- A Repository for Tarski-Kleene Algebras (with G. Struth, T. Weber), ATE 2011
- Towards a Typed Omega Algebra, RAMiCS 2011
- Unifying Recursion in Partial, Total and General Correctness, UTP 2010
- Partial, Total and General Correctness, MPC 2010
- Unifying the Semantics of UML 2 State, Activity and Interaction Diagrams (with J. Kohlmeyer), PSI 2009
- General Correctness Algebra, RelMiCS/AKA 2009
- Lazy UTP, UTP 2008
- Lazy Relations, RelMiCS/AKA 2008
- Algebraic Foundations of the Unifying Theories of Programming, 2007
- An ASM Semantics of Token Flow in UML 2 Activity Diagrams (with S. Sarstedt), PSI 2006
- Variations on an Ordering Theme with Constraints (with M. Maucher), TCS 2006
- Modal Design Algebra (with B. Möller), UTP 2006
- Non-termination in Unifying Theories of Programming, RelMiCS/AKA 2005

### Formally verified proof developments

- 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 Disjoint-Set Forests,
**AFP**, 2020 - Relational Characterisations of Paths (with P. Höfner),
**AFP**, 2020 - A Hierarchy of Algebras for Boolean Subsets (with B. Möller),
**AFP**, 2020 - Aggregation Algebras,
**AFP**, 2018 - Stone-Kleene Relation Algebras,
**AFP**, 2017 - Stone Relation Algebras,
**AFP**, 2017 - Stone Algebras,
**AFP**, 2016 - Kleene Algebras with Domain (with V. B. F. Gomes, P. Höfner, G. Struth, T. Weber),
**AFP**, 2016

### All publications

The following links are provided:

- bib: BibTeX entry
- http: final version at the publisher's site
- .pdf: author's manuscript
- .html: site with additional information

[72] |
W. Guttmann.
Dependences between domain constructions in heterogeneous relation
algebras.
In R. Glück, L. Santocanale, and M. Winter, editors,
Relational and Algebraic Methods in Computer Science, volume 13896 of
Lecture Notes in Computer Science, pages 105–121. Springer, 2023.
[ bib |
http |
.pdf ]
We show the following dependences between relational domain constructions in the framework of heterogeneous relation algebras. If all power sets and subsets exist and objects are comparable, then all sums exist. If all sums exist and atoms are rectangular, then all products exist. If all atoms are rectangular, then all subsets exist if and only if all quotients exist. We give models with rectangular atoms which rule out further dependences between these constructions. |

[71] |
W. Guttmann and N. Robinson-O'Brien.
Relation-algebraic verification of Borůvka's minimum spanning
tree algorithm.
In U. Fahrenberg, M. Gehrke, L. Santocanale, and M. Winter, editors,
Relational and Algebraic Methods in Computer Science, volume 13027 of
Lecture Notes in Computer Science, pages 225–240. Springer, 2021.
[ bib |
http |
.pdf ]
Previous work introduced a relation-algebraic framework for reasoning about weighted-graph algorithms. We use this framework to prove partial correctness of a sequential version of Borůvka's minimum spanning tree algorithm. This is the first formal proof of correctness for this algorithm. We also discuss new abstractions that make it easier to reason about weighted graphs. |

[70] |
W. Guttmann.
Second-order properties of undirected graphs.
In U. Fahrenberg, M. Gehrke, L. Santocanale, and M. Winter, editors,
Relational and Algebraic Methods in Computer Science, volume 13027 of
Lecture Notes in Computer Science, pages 209–224. Springer, 2021.
[ bib |
http |
.pdf ]
We study second-order formalisations of graph properties expressed as first-order formulas in relation algebras extended with a Kleene star. The formulas quantify over relations while still avoiding quantification over elements of the base set. We formalise the property of undirected graphs being acyclic this way. This involves a study of various kinds of orientation of graphs. We also verify basic algorithms to constructively prove several second-order properties. |

[69] |
W. Guttmann.
Algebras for iteration, infinite executions and correctness of
sequential computations.
Archive of Formal Proofs, October 2021.
[ bib |
.html |
.pdf ]
We study models of state-based non-deterministic sequential computations and describe them using algebras. We propose algebras that describe iteration for strict and non-strict computations. They unify computation models which differ in the fixpoints used to represent iteration. We propose algebras that describe the infinite executions of a computation. They lead to a unified approximation order and results that connect fixpoints in the approximation and refinement orders. This unifies the semantics of recursion for a range of computation models. We propose algebras that describe preconditions and the effect of while-programs under postconditions. They unify correctness statements in two dimensions: one statement applies in various computation models to various correctness claims. |

[68] |
W. Guttmann.
Relational forests.
Archive of Formal Proofs, August 2021.
[ bib |
.html |
.pdf ]
We study second-order formalisations of graph properties expressed as first-order formulas in relation algebras extended with a Kleene star. The formulas quantify over relations while still avoiding quantification over elements of the base set. We formalise the property of undirected graphs being acyclic this way. This involves a study of various kinds of orientation of graphs. We also verify basic algorithms to constructively prove several second-order properties. |

[67] |
W. Guttmann and N. Robinson-O'Brien.
Relational minimum spanning tree algorithms.
Archive of Formal Proofs, December 2020.
[ bib |
.html |
.pdf ]
We verify the correctness of Prim's, Kruskal's and Borůvka's minimum spanning tree algorithms based on algebras for aggregation and minimisation. |

[66] |
R. Berghammer, H. Furusawa, W. Guttmann, and P. Höfner.
Relational characterisations of paths.
Journal of Logical and Algebraic Methods in Programming,
117:100590, December 2020.
[ bib |
http |
.pdf ]
Binary relations are one of the standard ways to encode, characterise and reason about graphs. Relation algebras provide equational axioms for a large fragment of the calculus of binary relations. Although relations are standard tools in many areas of mathematics and computing, researchers usually fall back to point-wise reasoning when it comes to arguments about paths in a graph. We present a purely algebraic way to specify different kinds of paths in Kleene relation algebras, which are relation algebras equipped with an operation for reflexive transitive closure. We study the relationship between paths with a designated root vertex and paths without such a vertex. Since we stay in first-order logic this development helps with mechanising proofs. To demonstrate the applicability of the algebraic framework we verify the correctness of three basic graph algorithms. All results of this paper are formally verified using the interactive proof assistant Isabelle/HOL. |

[65] |
W. Guttmann.
Relational disjoint set forests.
Archive of Formal Proofs, August 2020.
[ bib |
.html |
.pdf ]
We give a simple relation-algebraic semantics of read and write operations on associative arrays. The array operations seamlessly integrate with assignments in the Hoare-logic library. Using relation algebras and Kleene algebras we verify the correctness of an array-based implementation of disjoint-set forests with a naive union operation and a find operation with path compression. |

[64] |
W. Guttmann and P. Höfner.
Relational characterisations of paths.
Archive of Formal Proofs, July 2020.
[ bib |
.html |
.pdf ]
Binary relations are one of the standard ways to encode, characterise and reason about graphs. Relation algebras provide equational axioms for a large fragment of the calculus of binary relations. Although relations are standard tools in many areas of mathematics and computing, researchers usually fall back to point-wise reasoning when it comes to arguments about paths in a graph. We present a purely algebraic way to specify different kinds of paths in Kleene relation algebras, which are relation algebras equipped with an operation for reflexive transitive closure. We study the relationship between paths with a designated root vertex and paths without such a vertex. Since we stay in first-order logic this development helps with mechanising proofs. To demonstrate the applicability of the algebraic framework we verify the correctness of three basic graph algorithms. |

[63] |
W. Guttmann.
Reasoning about algebraic structures with implicit carriers in
Isabelle/HOL.
In N. Peltier and V. Sofronie-Stokkermans, editors, Automated
Reasoning, Part 2, volume 12167 of Lecture Notes in Computer Science,
pages 251–268. Springer, 2020.
[ bib |
http |
.pdf ]
We prove Chen and Grätzer's construction theorem for Stone algebras in Isabelle/HOL. The development requires extensive reasoning about algebraic structures in addition to reasoning in algebraic structures. We present an approach for this using classes and locales with implicit carriers. This involves using function liftings to implement some aspects of dependent types and using embeddings of algebras to inherit theorems. We also formalise a theory of filters based on partial orders. |

[62] |
W. Guttmann and B. Möller.
A hierarchy of algebras for Boolean subsets.
In U. Fahrenberg, P. Jipsen, and M. Winter, editors, Relational
and Algebraic Methods in Computer Science, volume 12062 of Lecture
Notes in Computer Science, pages 152–168. Springer, 2020.
[ bib |
http |
.pdf ]
We present a collection of axiom systems for the construction of Boolean subalgebras of larger overall algebras. The subalgebras are defined as the range of a complement-like operation on a semilattice. This technique has been used, for example, with the antidomain operation, dynamic negation and Stone algebras. We present a common ground for these constructions based on a new equational axiomatisation of Boolean algebras. All results are formally proved in Isabelle/HOL. |

[61] |
W. Guttmann.
Verifying the correctness of disjoint-set forests with Kleene
relation algebras.
In U. Fahrenberg, P. Jipsen, and M. Winter, editors, Relational
and Algebraic Methods in Computer Science, volume 12062 of Lecture
Notes in Computer Science, pages 134–151. Springer, 2020.
[ bib |
http |
.pdf ]
We give a simple relation-algebraic semantics of read and write operations on associative arrays. The array operations seamlessly integrate with assignments in computation models supporting while-programs. As a result, relation algebras can be used for verifying programs with associative arrays. We verify the correctness of an array-based implementation of disjoint-set forests with a naive union operation and a find operation with path compression. All results are formally proved in Isabelle/HOL. |

[60] |
W. Guttmann and B. Möller.
A hierarchy of algebras for Boolean subsets.
Archive of Formal Proofs, January 2020.
[ bib |
.html |
.pdf ]
We present a collection of axiom systems for the construction of Boolean subalgebras of larger overall algebras. The subalgebras are defined as the range of a complement-like operation on a semilattice. This technique has been used, for example, with the antidomain operation, dynamic negation and Stone algebras. We present a common ground for these constructions based on a new equational axiomatisation of Boolean algebras. |

[59] |
W. Guttmann.
Connecting fixpoints of computations with strict progress.
In P. Ribeiro and A. Sampaio, editors, Unifying Theories of
Programming, Seventh International Symposium, UTP 2019, volume 11885 of
Lecture Notes in Computer Science, pages 62–79. Springer, 2019.
[ bib |
http |
.pdf ]
We study the semantics of recursion for computations that make strict progress. The underlying unified computation model has an abstract notion of progress, which instantiates in ways such as longer traces, passing of real time, or counting the number of steps. Recursion is given by least fixpoints in a unified approximation order. Other time-based models define the semantics of recursion by greatest fixpoints in the implication order. We give sufficient criteria for when least fixpoints in the approximation order coincide with greatest fixpoints in the implication order. |

[58] |
W. Guttmann.
Verifying minimum spanning tree algorithms with Stone relation
algebras.
Journal of Logical and Algebraic Methods in Programming,
101:132–150, December 2018.
[ bib |
http |
.pdf ]
We study a generalisation of relation algebras in which the underlying Boolean algebra structure is replaced with a Stone algebra. Many theorems of relation algebras generalise with no or small changes. Weighted graphs represented as matrices over extended real numbers form an instance. Relational concepts and methods can thus be applied to weighted graphs. We formally specify the problem of computing minimum spanning forests and express Kruskal's algorithm in relation-algebraic terms. We give a total-correctness proof of the algorithm. All results are formally verified in Isabelle/HOL. This paper is an extended version of [53]. |

[57] |
J. Desharnais, W. Guttmann, and S. Joosten, editors.
Relational and Algebraic Methods in Computer Science (RAMiCS
2018), volume 11194 of Lecture Notes in Computer Science. Springer,
2018.
[ bib |
http ]
This book constitutes the proceedings of the 17th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2018, held in Groningen, The Netherlands, in October/November 2018. |

[56] |
W. Guttmann.
An algebraic framework for minimum spanning tree problems.
Theoretical Computer Science, 744:37–55, October 2018.
[ bib |
http |
.pdf ]
We formally prove that Prim's minimum spanning tree algorithm is correct for various optimisation problems with different aggregation functions. The original minimum weight spanning tree problem and the minimum bottleneck spanning tree problem are special cases, but the framework covers many other problems. To this end we work in new generalisations of relation algebras and Kleene algebras and in new algebraic structures that capture key operations used in Prim's algorithm and its specification. Weighted graphs form instances of these algebraic structures, where edge weights are taken from a linear order with a binary aggregation operation. Many existing results from relation algebras and Kleene algebras generalise from the relation model to the weighted-graph model with no or small changes. The overall structure of the proof uses Hoare logic. All results are formally verified in Isabelle/HOL heavily using its integrated automated theorem provers. This paper is an extended version of [49]. |

[55] |
W. Guttmann.
Aggregation algebras.
Archive of Formal Proofs, September 2018.
[ bib |
.html |
.pdf ]
We develop algebras for aggregation and minimisation for weight matrices and for edge weights in graphs. We verify the correctness of Prim's and Kruskal's minimum spanning tree algorithms based on these algebras. We also show numerous instances of these algebras based on linearly ordered commutative semigroups. |

[54] |
W. Guttmann.
Stone-Kleene relation algebras.
Archive of Formal Proofs, October 2017.
[ bib |
.html |
.pdf ]
We develop Stone-Kleene relation algebras, which expand Stone relation algebras with a Kleene star operation to describe reachability in weighted graphs. Many properties of the Kleene star arise as a special case of a more general theory of iteration based on Conway semirings extended by simulation axioms. This includes several theorems representing complex program transformations. We formally prove the correctness of Conway's automata-based construction of the Kleene star of a matrix. We prove numerous results useful for reasoning about weighted graphs. |

[53] |
W. Guttmann.
Stone relation algebras.
In P. Höfner, D. Pous, and G. Struth, editors, Relational
and Algebraic Methods in Computer Science (RAMiCS 2017), volume 10226 of
Lecture Notes in Computer Science, pages 127–143. Springer, 2017.
[ bib |
http |
.pdf ]
We study a generalisation of relation algebras in which the underlying Boolean algebra structure is replaced with a Stone algebra. Many theorems of relation algebras generalise with no or small changes. Weighted graphs represented as matrices over extended real numbers form an instance. Relational concepts and methods can thus be applied to weighted graphs. All results are formally verified in Isabelle/HOL. |

[52] |
R. Berghammer and W. Guttmann.
An algebraic approach to multirelations and their properties.
Journal of Logical and Algebraic Methods in Programming,
88:45–63, April 2017.
[ bib |
http |
.pdf ]
We study operations and equational properties of multirelations, which have been used for modelling games, protocols, computations, contact, closure and topology. The operations and properties are expressed using sets, heterogeneous relation algebras and more general algebras for multirelations. We investigate the algebraic properties of a new composition operation based on the correspondence to predicate transformers, different ways to express reflexive-transitive closures of multirelations, numerous equational properties, how these properties are connected and their preservation by multirelational operations. We particularly aim to generalise results and properties from up-closed multirelations to arbitrary multirelations. This paper is an extended version of [45]. |

[51] |
M. Ge, J. B. Hong, W. Guttmann, and D. S. Kim.
A framework for automating security analysis of the Internet of
Things.
Journal of Network and Computer Applications, 83:12–27, April
2017.
[ bib |
http |
.pdf ]
The Internet of Things (IoT) is enabling innovative applications in various domains. Due to its heterogeneous and wide-scale structure, it introduces many new security issues. To address this problem, we propose a framework for modeling and assessing the security of the IoT and provide a formal definition of the framework. Generally, the framework consists of five phases: (1) data processing, (2) security model generation, (3) security visualization, (4) security analysis, and (5) model updates. Using the framework, we can find potential attack scenarios in the IoT, analyze the security of the IoT through well-defined security metrics, and assess the effectiveness of different defense strategies. The framework is evaluated via three scenarios, which are the smart home, wearable healthcare monitoring and environment monitoring scenarios. We use the analysis results to show the capabilities of the proposed framework for finding potential attack paths and mitigating the impact of attacks. |

[50] |
W. Guttmann.
Stone relation algebras.
Archive of Formal Proofs, February 2017.
[ bib |
.html |
.pdf ]
We develop Stone relation algebras, which generalise relation algebras by replacing the underlying Boolean algebra structure with a Stone algebra. We show that finite matrices over extended real numbers form an instance. As a consequence, relation-algebraic concepts and methods can be used for reasoning about weighted graphs. We also develop a fixpoint calculus and apply it to compare different definitions of reflexive-transitive closures in semirings. |

[49] |
W. Guttmann.
Relation-algebraic verification of Prim's minimum spanning tree
algorithm.
In A. Sampaio and F. Wang, editors, Theoretical Aspects of
Computing – ICTAC 2016, volume 9965 of Lecture Notes in Computer
Science, pages 51–68. Springer, 2016.
[ bib |
http |
.pdf ]
We formally prove the correctness of Prim's algorithm for computing minimum spanning trees. We introduce new generalisations of relation algebras and Kleene algebras, in which most of the proof can be carried out. Only a small part needs additional operations, for which we introduce a new algebraic structure. We instantiate these algebras by matrices over extended reals, which model the weighted graphs used in the algorithm. Many existing results from relation algebras and Kleene algebras generalise from the relation model to the weighted-graph model with no or small changes. The overall structure of the proof uses Hoare logic. All results are formally verified in Isabelle/HOL heavily using its integrated automated theorem provers. |

[48] |
W. Guttmann.
Stone algebras.
Archive of Formal Proofs, September 2016.
[ bib |
.html |
.pdf ]
A range of algebras between lattices and Boolean algebras generalise the notion of a complement. We develop a hierarchy of these pseudo-complemented algebras that includes Stone algebras. Independently of this theory we study filters based on partial orders. Both theories are combined to prove Chen and Grätzer's construction theorem for Stone algebras. The latter involves extensive reasoning about algebraic structures in addition to reasoning in algebraic structures. |

[47] |
W. Guttmann.
An algebraic approach to computations with progress.
Journal of Logical and Algebraic Methods in Programming,
85(4):520–539, June 2016.
[ bib |
http |
.pdf ]
The notion of progress appears in various computation models, for example, in the form of traces getting longer, passing of real time, incrementing a counter, going from termination to non-termination. We introduce a model of sequential computations that generalises and abstracts these examples. We generalise existing algebras for non-terminating executions and instantiate these with our model. Using these algebras we derive an approximation order for computations with time and for trace-based computations. We introduce a generalisation of omega algebras to express iteration in the new model. |

[46] |
V. B. F. Gomes, W. Guttmann, P. Höfner, G. Struth, and T. Weber.
Kleene algebras with domain.
Archive of Formal Proofs, April 2016.
[ bib |
.html |
.pdf ]
Kleene algebras with domain are Kleene algebras endowed with an operation that maps each element of the algebra to its domain of definition (or its complement) in abstract fashion. They form a simple algebraic basis for Hoare logics, dynamic logics or predicate transformer semantics. We formalise a modular hierarchy of algebras with domain and antidomain (domain complement) operations in Isabelle/HOL that ranges from domain and antidomain semigroups to modal Kleene algebras and divergence Kleene algebras. We link these algebras with models of binary relations and program traces. We include some examples from modal logics, termination and program analysis. |

[45] |
R. Berghammer and W. Guttmann.
Closure, properties and closure properties of multirelations.
In W. Kahl, M. Winter, and J. N. Oliveira, editors, Relational
and Algebraic Methods in Computer Science, volume 9348 of Lecture Notes
in Computer Science, pages 67–83. Springer, 2015.
[ bib |
http |
.pdf ]
Multirelations have been used for modelling games, protocols and computations. They have also been used for modelling contact, closure and topology. We bring together these two lines of research using relation algebras and more general algebras. In particular, we look at various properties of multirelations that have been used in the two lines of research, show how these properties are connected and study by which multirelational operations they are preserved. We find that many results do not require a restriction to up-closed multirelations; this includes connections between various kinds of reflexive-transitive closure. |

[44] |
R. Berghammer and W. Guttmann.
A relation-algebraic approach to multirelations and predicate
transformers.
In R. Hinze and J. Voigtländer, editors, Mathematics of
Program Construction, volume 9129 of Lecture Notes in Computer
Science, pages 50–70. Springer, 2015.
[ bib |
http |
.pdf ]
The correspondence between up-closed multirelations and isotone predicate transformers is well known. Less known is that multirelations have also been used for modelling topological contact, not only computations. We investigate how properties from these two lines of research translate to predicate transformers. To this end, we express the correspondence of multirelations and predicate transformers using relation algebras. It turns out to be similar to the correspondence between contact relations and closure operations. Many results generalise from up-closed to arbitrary multirelations. |

[43] |
W. Guttmann.
Infinite executions of lazy and strict computations.
Journal of Logical and Algebraic Methods in Programming,
84(3):326–340, May 2015.
[ bib |
http |
.pdf ]
We give axioms for an operation that describes the states from which a computation has infinite executions in several relational and matrix-based models. The models cover non-strict and strict computations which represent finite, infinite and aborting executions with varying precision. Based on the operation we provide an approximation order for a unified description of recursion. Least fixpoints in the approximation order are reduced to least and greatest fixpoints in the underlying semilattice order. We specialise this to a unified description of iteration which satisfies the axioms of a binary operation introduced in previous work. Previous consequences therefore generalise to all discussed computation models in a uniform way. All algebraic results are verified in Isabelle using its integrated automated theorem provers and SMT solvers. |

[42] |
W. Guttmann.
Algebras for Iteration, Infinite Executions and Correctness of
Sequential Computations.
Habilitationsschrift, Universität Ulm, April 2015.
[ bib |
.pdf ]
We study models of state-based non-deterministic sequential computations. They differ in the kinds of computation they can represent and the precision they achieve. We systematically explore existing models, propose new models and investigate their connections. We propose algebras that describe iteration for strict and non-strict computations. They enable a unified treatment of various computation models which greatly differ in the fixpoints used to represent iteration. Our axioms are general enough to capture the semantics of while-loops in all of these models, yet powerful enough to derive complex results including program transformations and refinement theorems. We propose algebras that describe the infinite executions of a computation. In these algebras we define a unified approximation order, which applies to a wide variety of computation models. We thus obtain a unified semantics of recursion and results that connect fixpoints in the approximation and refinement orders. These results simplify reasoning about recursion and seamlessly match with our algebras for iteration when specialised to this case. We propose algebras that describe preconditions and the effect of while-programs under postconditions. Based on these we unify correctness statements in two dimensions: one statement applies in various computation models to various correctness claims. Despite their generality and the weakness of the underlying axioms we can give a sound and relatively complete correctness calculus. It also covers computation models in which choices are made by two interacting agents. The overarching algebraic method is to identify key aspects of computations, to describe these aspects by operations of algebras and to capture their properties by axioms. Theorems derived from these axioms express program transformations, correctness statements and refinement laws. We strive towards weaker axioms so as to capture more computation models. Reasoning about programs and specifications amounts to reasoning in the algebras, which can be supported by automated theorem proving technology. We extensively apply such tools to structure our results and to ensure their correctness. |

[41] |
W. Guttmann.
Isabelle/HOL theories of algebras for iteration, infinite
executions and correctness of sequential computations.
Technical Report TR-COSC 02/15, University of Canterbury, April
2015.
[ bib |
.html |
.pdf ]
This technical report contains Isabelle/HOL theories that describe algebras for iteration, infinite executions and correctness of sequential computations. The results are explained in a separate document. The Isabelle/HOL theory files are available at http://www.csse.canterbury.ac.nz/research/reports/TechReps/2015/tr_1502_theories.zip. |

[40] |
W. Guttmann.
Algebras for correctness of sequential computations.
Science of Computer Programming, 85(Part B):224–240, June
2014.
[ bib |
http |
.pdf ]
Previous work gives algebras for uniformly describing correctness statements and calculi in various relational and matrix-based computation models. These models support a single kind of non-determinism, which is either angelic, demonic or erratic with respect to the infinite executions of a computation. Other models, notably isotone predicate transformers or up-closed multirelations, offer both angelic and demonic choice with respect to finite executions. We propose algebras for a theory of correctness which covers these multirelational models in addition to relational and matrix-based models. Existing algebraic descriptions, in particular general refinement algebras and monotonic Boolean transformers, are instances of our theory. Our new description includes a precondition operation that instantiates to both modal diamond and modal box operators. We verify all results in Isabelle, heavily using its automated theorem provers. We integrate our theories with the Isabelle theory of monotonic Boolean transformers making our results applicable to that setting. |

[39] |
W. Guttmann.
Extended conscriptions algebraically.
In P. Höfner, P. Jipsen, W. Kahl, and M. E. Müller, editors,
Relational and Algebraic Methods in Computer Science, volume 8428 of
Lecture Notes in Computer Science, pages 139–156. Springer, 2014.
[ bib |
http |
.pdf ]
Conscriptions are a model of sequential computations with assumption/commitment specifications in which assumptions can refer to final states, not just to initial states. We show that they instantiate existing algebras for iteration and infinite computations. We use these algebras to derive an approximation order for conscriptions and one for extended conscriptions, which additionally represent aborting executions. We give a new computation model which generalises extended conscriptions and apply the algebraic techniques for a unified treatment. |

[38] |
W. Guttmann.
Multirelations with infinite computations.
Journal of Logical and Algebraic Methods in Programming,
83(2):194–211, March 2014.
[ bib |
http |
.pdf ]
Multirelations model computations with both angelic and demonic non-determinism. We extend multirelations to represent finite and infinite computations independently. We derive an approximation order for multirelations assuming only that the endless loop is its least element and that the lattice operations are isotone. We use relations, relation algebra and RelView for representing and calculating with multirelations and for finding the approximation order. |

[37] |
W. Guttmann.
Extended designs algebraically.
Science of Computer Programming, 78(11):2064–2085, November
2013.
[ bib |
http |
.pdf ]
Extended designs distinguish non-terminating and aborting executions of sequential, non-deterministic programs. We show how to treat them algebraically based on techniques we have previously applied to total and general correctness approaches. In particular, we propose modifications to the definition of an extended design which make the theory more clear and simplify calculations, and an approximation order for recursion. We derive explicit formulas for operators on extended designs including non-deterministic choice, sequential composition, while-loops and full recursion. We show how to represent extended designs as designs or prescriptions over an extended state space. The new theory generalises our previous algebraic theory of general correctness by weakening its axioms. It also integrates with partial, total and general correctness into a common foundation which gives a unified semantics of while-programs. Program transformations derived using this semantics are valid in all four correctness approaches. |

[36] |
W. Guttmann.
Unifying lazy and strict computations.
In W. Kahl and T. G. Griffin, editors, Relational and Algebraic
Methods in Computer Science, volume 7560 of Lecture Notes in Computer
Science, pages 17–32. Springer, 2012.
[ bib |
http |
.pdf ]
Non-strict sequential computations describe imperative programs that can be executed lazily and support infinite data structures. Based on a relational model of such computations we investigate their algebraic properties. We show that they share many laws with conventional, strict computations. We develop a common theory generalising previous algebraic descriptions of strict computation models including partial, total and general correctness and extensions thereof. Due to non-strictness, the iteration underlying loops cannot be described by a unary operation. We propose axioms that generalise the binary operation known from omega algebra, and derive properties of this new operation which hold for both strict and non-strict computations. All algebraic results are verified in Isabelle using its integrated automated theorem provers. |

[35] |
W. Guttmann.
Algebras for iteration and infinite computations.
Acta Informatica, 49(5):343–359, August 2012.
[ bib |
http |
.pdf ]
We give axioms for an operation that describes iteration in various relational models of computations. The models differ in their treatment of finite, infinite and aborting executions, covering partial, total and general correctness and extensions thereof. Based on the common axioms we derive separation, refinement and program transformation results hitherto known from particular models, henceforth recognised to hold in many different models. We introduce a new model that independently describes the finite, infinite and aborting executions of a computation, and axiomatise an operation that extracts the infinite executions in this model and others. From these unifying axioms we derive explicit representations for recursion and iteration. We show that also the new model is an instance of our general theory of iteration. All results are verified in Isabelle heavily using automated theorem provers. |

[34] |
W. Guttmann.
Typing theorems of omega algebra.
Journal of Logic and Algebraic Programming, 81(6):643–659,
August 2012.
[ bib |
http |
.pdf ]
Typed omega algebras extend Kozen's typed Kleene algebras by an operation for infinite iteration in a similar way as Cohen's omega algebras extend Kleene algebras in the untyped case. Typing these algebras is motivated by non-square matrices in automata constructions and applications in program semantics. For several reasons - the theory of untyped (Kleene or omega) algebras is well developed, results are easier to derive, and automation support is much better - it is beneficial to transfer theorems from the untyped algebras to their typed variants instead of constructing new proofs in the typed setting. Such a typing of theorems is facilitated by embedding typed algebras into their untyped variants. Extending previous work, we show that a large class of theorems of 1-free omega algebras can be transferred to typed omega algebras. This covers every universal 1-free formula which does not contain the greatest element at the beginning of an expression in a negative occurrence of an equation. Moreover, the formulas may be infinitary. |

[33] |
W. Guttmann.
Unifying correctness statements.
In J. Gibbons and P. Nogueira, editors, Mathematics of Program
Construction, volume 7342 of Lecture Notes in Computer Science, pages
198–219. Springer, 2012.
[ bib |
http |
.pdf ]
Partial, total and general correctness and further models of sequential computations differ in their treatment of finite, infinite and aborting executions. Algebras structure this diversity of models to avoid the repeated development of similar theories and to clarify their range of application. We introduce algebras that uniformly describe correctness statements, correctness calculi, pre-post specifications and loop refinement rules in five kinds of computation models. This extends previous work that unifies iteration, recursion and program transformations for some of these models. Our new description includes a relativised domain operation, which ignores parts of a computation, and represents bound functions for claims of termination by sequences of tests. We verify all results in Isabelle heavily using its automated theorem provers. |

[32] |
W. Guttmann, G. Struth, and T. Weber.
Automating algebraic methods in Isabelle.
In S. Qin and Z. Qiu, editors, Formal Methods and Software
Engineering, volume 6991 of Lecture Notes in Computer Science, pages
617–632. Springer, 2011.
[ bib |
http |
.pdf ]
We implement a large Isabelle/HOL repository of algebras for application in modelling computing systems. They subsume computational logics such as dynamic and Hoare logics and form a basis for various software development methods. Isabelle has recently been extended by automated theorem provers and SMT solvers. We use these integrated tools for automatically proving several rather intricate refinement and termination theorems. We also automate a modal correspondence result and soundness and relative completeness proofs of propositional Hoare logic. These results show, for the first time, that Isabelle's tool integration makes automated algebraic reasoning particularly simple. This is a step towards increasing the automation of formal methods. |

[31] |
W. Guttmann.
Fixpoints for general correctness.
Journal of Logic and Algebraic Programming, 80(6):248–265,
August 2011.
[ bib |
http |
.pdf ]
We investigate various fixpoint operators in a semiring-based setting that models a general correctness semantics of programs. They arise as combinations of least/greatest (pre/post) fixpoints with respect to refinement/approximation. In particular, we show isotony of these operators and give representations of fixpoints in terms of other fixpoints. Some results require completeness of the Egli-Milner order, for which we provide conditions. A new perspective is reached by exchanging the semirings with distributive lattices. They can be augmented in a natural way with a second order that is similar to the Egli-Milner order. We extend our discussion of fixpoint operators to this induced order. We show the impact on general correctness by connecting the lattice- and the semiring-based treatments to obtain results about the Egli-Milner order. |

[30] |
W. Guttmann, G. Struth, and T. Weber.
A repository for Tarski-Kleene algebras.
In P. Höfner, A. McIver, and G. Struth, editors, Automated
Theory Engineering, volume 760 of CEUR Workshop Proceedings, pages
30–39, 2011.
[ bib |
http |
.pdf ]
We have implemented a repository of algebraic structures and theorems in the theorem proving environment Isabelle/HOL. It covers variants of Kleene algebras and relation algebras with many of their models. Most theorems have been obtained by automated theorem proving within Isabelle. Main purposes of the repository are the engineering of algebraic theories for computing systems and their application in formal program development. This paper describes the present state of the repository, illustrates its potential by a theory engineering and a program verification example, and discusses the most important directions for future work. |

[29] |
W. Guttmann.
Towards a typed omega algebra.
In H. de Swart, editor, Relational and Algebraic Methods in
Computer Science, volume 6663 of Lecture Notes in Computer Science,
pages 196–211. Springer, 2011.
[ bib |
http |
.pdf ]
We propose axioms for 1-free omega algebra, typed 1-free omega algebra and typed omega algebra. They are based on Kozen's axioms for 1-free and typed Kleene algebra and Cohen's axioms for the omega operation. In contrast to Kleene algebra, several laws of omega algebra turn into independent axioms in the typed or 1-free variants. We set up a matrix algebra over typed 1-free omega algebras by lifting the underlying structure. The algebra includes non-square matrices and care has to be taken to preserve type-correctness. The matrices can represent programs in total and general correctness. We apply the typed construction to derive the omega operation on two such representations, for which the untyped construction does not work. We embed typed 1-free omega algebra into 1-free omega algebra, and this into omega algebra. Some of our embeddings, however, do not preserve the greatest element. We obtain that the validity of a universal formula using only +, ⋅, |

[28] |
W. Guttmann.
Unifying recursion in partial, total and general correctness.
In S. Qin, editor, Unifying Theories of Programming, Third
International Symposium, UTP 2010, volume 6445 of Lecture Notes in
Computer Science, pages 207–225. Springer, 2010.
[ bib |
http |
.pdf ]
We give an algebraic semantics of non-deterministic, sequential programs which is valid for partial, total and general correctness. It covers full recursion based on a unified approximation order. We provide explicit solutions in terms of the refinement order. As an application, we systematically derive a semantics of while-programs common to the three correctness approaches. UTP's designs and prescriptions represent programs as pairs of termination and state transition information in total and general correctness, respectively. We show that our unified semantics induces a pair-based representation which is common to the correctness approaches. Operations on the pairs, including finite and infinite iteration, can be derived systematically. We also provide the effect of full recursion on the unified, pair-based representation. |

[27] |
W. Guttmann.
Imperative abstractions for functional actions.
Journal of Logic and Algebraic Programming, 79(8):768–793,
November 2010.
[ bib |
http |
.pdf ]
We elaborate our relational model of non-strict, imperative computations. The theory is extended to support infinite data structures. To facilitate their use in programs, we extend the programming language by concepts such as procedures, parameters, partial application, algebraic data types, pattern matching and list comprehensions. For each concept, we provide a relational semantics. Abstraction is further improved by programming patterns such as fold, unfold and divide-and-conquer. To support program reasoning, we prove laws such as fold-map fusion, otherwise known from functional programming languages. We give examples to show the use of our concepts in programs. |

[26] |
W. Guttmann.
Lazy UTP.
In A. Butterfield, editor, Unifying Theories of Programming,
Second International Symposium, UTP 2008, volume 5713 of Lecture Notes
in Computer Science, pages 82–101. Springer, 2010.
[ bib |
http |
.pdf ]
We integrate non-strict computations into the Unifying Theories of Programming. After showing that this is not possible with designs, we develop a new relational model representing undefinedness independently of non-termination. The relations satisfy additional healthiness conditions that model dependence in computations in an elegant algebraic form using partial orders. Programs can be executed according to the principle of lazy evaluation, otherwise known from functional programming languages. We extend the theory to support infinite data structures and give examples to show their use in programs. |

[25] |
W. Guttmann.
Partial, total and general correctness.
In C. Bolduc, J. Desharnais, and B. Ktari, editors, Mathematics
of Program Construction, volume 6120 of Lecture Notes in Computer
Science, pages 157–177. Springer, 2010.
[ bib |
http |
.pdf ]
We identify weak semirings, which drop the right annihilation axiom a0 = 0, as a common foundation for partial, total and general correctness. It is known how to extend weak semirings by operations for finite and infinite iteration and domain. We use the resulting weak omega algebras with domain to define a semantics of while-programs which is valid in all three correctness approaches. The unified, algebraic semantics yields program transformations at once for partial, total and general correctness. We thus give a proof of the normal form theorem for while-programs, which is a new result for general correctness and extends to programs with non-deterministic choice. By adding specific axioms to the common ones, we obtain partial, total or general correctness as a specialisation. We continue our previous investigation of axioms for general correctness. In particular, we show that a subset of these axioms is sufficient to derive a useful theory, which includes the Egli-Milner order, full recursion, correctness statements and a correctness calculus. We also show that this subset is necessary. |

[24] |
W. Guttmann and B. Möller.
Normal design algebra.
Journal of Logic and Algebraic Programming, 79(2):144–173,
February 2010.
[ bib |
http |
.pdf ]
We generalise the designs of the Unifying Theories of Programming (UTP) by defining them as matrices over semirings with ideals. This clarifies the algebraic structure of designs and considerably simplifies reasoning about them, for example, since they form a Kleene and omega algebra and a test semiring. We apply our framework to investigate symmetric linear recursion and its relation to tail-recursion. This substantially involves Kleene and omega algebra as well as additional algebraic formulations of determinacy, invariants, domain, pre-image, convergence and Noetherity. Due to the uncovered algebraic structure of UTP designs, all our general results also directly apply to UTP. |

[23] |
J. Kohlmeyer and W. Guttmann.
Unifying the semantics of UML 2 state, activity and interaction
diagrams.
In A. Pnueli, I. Virbitskaite, and A. Voronkov, editors,
Perspectives of System Informatics: 7th International Andrei Ershov Memorial
Conference, PSI 2009, volume 5947 of Lecture Notes in Computer
Science, pages 206–217. Springer, 2010.
[ bib |
http |
.pdf ]
We define a formal semantics of the combined use of UML 2 state machines, activities and interactions using Abstract State Machines. The behaviour of software models can henceforth be specified by composing these diagrams, choosing the most adequate formalism at each level of abstraction. We present several reasonable ways to link different kinds of diagrams and illustrate them by examples. We also give a formal semantics of communication between these diagrams. The resulting rules reveal unclear parts of the UML specification and serve as a basis for tool support. |

[22] |
W. Guttmann.
General correctness algebra.
In R. Berghammer, A. M. Jaoua, and B. Möller, editors,
Relations and Kleene Algebra in Computer Science, volume 5827 of
Lecture Notes in Computer Science, pages 150–165. Springer, 2009.
[ bib |
http |
.pdf ]
General correctness offers a finer semantics of programs than partial and total correctness. We give an algebraic account continuing and extending previous approaches. In particular, we propose axioms, correctness statements, a correctness calculus, specification constructs and a loop refinement rule. The Egli-Milner order is treated algebraically and we show how to obtain least fixpoints, used to solve recursion equations, in terms of the natural order. |

[21] |
J. Kohlmeyer and W. Guttmann.
Unifying the semantics of UML 2 state, activity and interaction
diagrams.
In A. Pnueli, I. Virbitskaite, and A. Voronkov, editors,
Perspectives of System Informatics: Proceedings of the Seventh International
Andrei Ershov Memorial Conference, pages 159–166. A. P. Ershov Institute of
Informatics Systems, Novosibirsk, June 2009.
[ bib ]
This is a preliminary version of [23]. |

[20] |
W. Guttmann.
Lazy UTP.
In A. Butterfield, editor, Second International Symposium on the
Unifying Theories of Programming (UTP 08), pages 253–272. Trinity College
Dublin, Ireland, September 2008.
[ bib ]
This is a preliminary version of [26]. |

[19] |
W. Guttmann.
Algebraic foundations of the Unifying Theories of Programming.
In D. Wagner et al., editors, Ausgezeichnete
Informatikdissertationen 2007, volume D-8 of Lecture Notes in
Informatics, pages 141–150. Gesellschaft für Informatik, 2008.
[ bib ]
This summary of [17] was invited as it was short-listed for the dissertation award of the German computer science society GI. |

[18] |
W. Guttmann.
Lazy relations.
In R. Berghammer, B. Möller, and G. Struth, editors,
Relations and Kleene Algebra in Computer Science, volume 4988 of
Lecture Notes in Computer Science, pages 138–154. Springer, 2008.
[ bib |
http |
.pdf ]
We present a relational model of non-strict computations in an imperative, non-deterministic context. Undefinedness is represented independently of non-termination. The relations satisfy algebraic properties known from other approaches to model imperative programs; we introduce additional laws that model dependence in computations in an elegant algebraic form using partial orders. Programs can be executed according to the principle of lazy evaluation, otherwise known from functional programming languages. Local variables are treated by relational parallel composition. |

[17] |
W. Guttmann.
Algebraic Foundations of the Unifying Theories of Programming.
Dissertation, Universität Ulm, December 2007.
[ bib |
http |
.pdf ]
Hoare and He's Unifying Theories of Programming take a relational view on semantics. The meaning of a non-deterministic, imperative program is described by 'designs' composed of two relations. They represent terminating states and relate the initial and final values of the observable variables, respectively. Several 'healthiness conditions' are imposed by the theory to obtain properties found in practice. This work determines the structure of designs and modifies the theory to support non-strict computations. It achieves these goals by identifying healthiness conditions and related axioms that involve unnecessary restrictions and subsequently removing them. The outcome provides a clear account of the algebraic foundations of the Unifying Theories of Programming. One of the results is a generalisation of designs by constructing them on semirings with ideals, structures having fewer axioms than relations. This clarifies the essential algebraic structure of designs, allows the reuse of existing mathematical theory and connects to further semantical approaches. The framework is extended by algebraic formulations of finite and infinite iteration, domain, pre-image, determinacy, invariants and convergence. Calculations and reasoning become simpler by the new, more abstract representation as is shown by applying the theory to investigate linear recursions. Another result is an extension of the Unifying Theories of Programming to deal with undefined values irrespective of non-termination. Besides being closer to practice, it forms the basis of a new theory of relations representing non-strict computations. They satisfy additional healthiness conditions that model dependence in computations in an elegant algebraic form. Programs can then be executed according to the principle of lazy evaluation, otherwise known from functional programming languages. |

[16] |
S. Sarstedt and W. Guttmann.
An ASM semantics of token flow in UML 2 activity diagrams.
In I. Virbitskaite and A. Voronkov, editors, Perspectives of
System Informatics: 6th International Andrei Ershov Memorial Conference, PSI
2006, volume 4378 of Lecture Notes in Computer Science, pages
349–362. Springer, 2007.
[ bib |
http |
.pdf ]
The token flow semantics of UML 2 activity diagrams is formally defined using Abstract State Machines. Interruptible activity regions and multiplicity bounds for pins are considered for the first time in a comprehensive and rigorous way. The formalisation provides insight into problems with the UML specification, and their solutions. It also serves as a basis for an integrated environment supporting the simulation and debugging of activity diagrams. |

[15] |
W. Guttmann and B. Möller.
Normal design algebra.
Technical Report 2006-28, Institut für Informatik,
Universität Augsburg, December 2006.
[ bib |
http |
.pdf ]
We generalise the designs of Unifying Theories of Programming (UTP) by defining them as matrices over semirings with ideals. This clarifies the algebraic structure of designs and considerably simplifies reasoning about them, e.g., forming a Kleene and omega algebra of designs. Moreover, we prove a generalised fixpoint theorem for isotone functions on designs. We apply our framework to investigate symmetric linear recursion and its relation to tail-recursion; this substantially involves Kleene and omega algebra as well as additional algebraic formulations of determinacy, invariants, domain, pre-image, convergence and noetherity. Due to the uncovered algebraic structure of UTP designs, all our general results also directly apply to UTP. This technical report accompanies [24]. |

[14] |
W. Guttmann and M. Maucher.
Variations on an ordering theme with constraints.
In G. Navarro, L. Bertossi, and Y. Kohayakawa, editors, Fourth
IFIP International Conference on Theoretical Computer Science: TCS 2006,
volume 209 of IFIP International Federation for Information Processing,
pages 77–90. Springer, 2006.
[ bib |
http |
.pdf ]
We investigate the problem of finding a total order of a finite set that satisfies various local ordering constraints. Depending on the admitted constraints, we provide an efficient algorithm or prove NP-completeness. We discuss several generalisations and systematically classify the problems. |

[13] |
S. Sarstedt and W. Guttmann.
An ASM semantics of token flow in UML 2 activity diagrams.
In I. Virbitskaite and A. Voronkov, editors, Perspectives of
System Informatics: Proceedings of the Sixth International Andrei Ershov
Memorial Conference, pages 207–213. A. P. Ershov Institute of Informatics
Systems, Novosibirsk, June 2006.
[ bib ]
This is a preliminary version of [16]. |

[12] |
W. Guttmann and B. Möller.
Modal design algebra.
In S. Dunne and W. Stoddart, editors, Unifying Theories of
Programming, volume 4010 of Lecture Notes in Computer Science, pages
236–256. Springer, 2006.
[ bib |
http |
.pdf ]
We give an algebraic model of the designs of UTP based on a variant of modal semirings, hence generalising the original relational model. This is intended to exhibit more clearly the algebraic principles behind UTP and to provide deeper insight into the general properties of designs, the program and specification operators, and refinement. Moreover, we set up a formal connection with general and total correctness of programs as discussed by a number of authors. Finally we show that the designs form a left semiring and even a Kleene and omega algebra. This is used to calculate closed expressions for the least and greatest fixed-point semantics of the demonic while loop that are simpler than the ones obtained from standard UTP theory and previous algebraic approaches. |

[11] |
W. Guttmann.
Non-termination in Unifying Theories of Programming.
In W. MacCaull, M. Winter, and I. Düntsch, editors,
Relational Methods in Computer Science 2005, volume 3929 of Lecture
Notes in Computer Science, pages 108–120. Springer, 2006.
[ bib |
http |
.pdf ]
Within the Unifying Theories of Programming framework, program initiation and termination has been modelled by introducing a pair of variables in order to satisfy the required algebraic properties. We replace these variables with the improper value ⊥ that is frequently used to denote undefinedness. Both approaches are proved isomorphic using the relation calculus, and the existing operations and laws are carried over. We split the isomorphism by interposing "intuitive" relations. |

[10] |
W. Guttmann and B. Möller.
Modal design algebra.
In S. Dunne and W. Stoddart, editors, First International
Symposium on the Unifying Theories of Programming (UTP 06), pages 206–225.
University of Teesside, United Kingdom, February 2006.
[ bib ]
This is a preliminary version of [12]. |

[9] |
W. Guttmann and M. Maucher.
Constrained ordering.
Technical Report UIB-2005-03, Universität Ulm, December 2005.
[ bib |
.html |
http |
.pdf ]
We investigate the problem of finding a total order of a finite set that satisfies various local ordering constraints. Depending on the admitted constraints, we provide an efficient algorithm or prove NP-completeness. To this end, we define a reduction technique and discuss its properties. This technical report accompanies [14]. |

[8] |
W. Guttmann and B. Möller.
Modal design algebra.
Technical Report 2005-15, Institut für Informatik,
Universität Augsburg, September 2005.
[ bib |
http |
.pdf ]
We give an algebraic model of (H3) designs based on a variant of modal semirings, hence generalising the original relational model. This makes the theory applicable to a wider class of settings, e.g., to algebras of sets of traces. Moreover, we set up the connection with the weakly and strongly demonic semantics of programs as discussed by a number of authors. This is done using commands (a,t) where a corresponds to the transition relation of a program and the condition t characterises the input states from which termination is guaranteed. The commands form not only a semiring but even a Kleene and omega algebra. This is used to calculate closed expressions for the least and greatest fixed point semantics of the demonic while loop. This technical report accompanies [12]. |

[7] |
W. Guttmann.
Non-termination in Unifying Theories of Programming.
In I. Düntsch and M. Winter, editors, 8th International
Conference on Relational Methods in Computer Science (RelMiCS 8), pages
87–94. Computer Science Department, Brock University, St. Catharines,
Ontario, Canada, February 2005.
[ bib ]
This is a preliminary version of [11]. |

[6] |
W. Guttmann, H. Partsch, W. Schulte, and T. Vullinghs.
Tool support for the interactive derivation of formally correct
functional programs.
Journal of Universal Computer Science, 9(2):173–188, March
2003.
[ bib |
http |
.pdf ]
This paper describes the program transformation system Ultra. The intended use of Ultra is to assist programmers in the formal derivation of correct and efficient programs from high-level descriptive or operational specifications. We illustrate its utility by deriving a version of the Heapsort algorithm from a non-deterministic specification. Ultra supports equational reasoning about functional programs using defining equations, algebraic laws of underlying data structures, and transformation rules. The system does not only support modifying terms, but is also useful for bookkeeping and development-navigating tasks. The most salient features of Ultra are its sound theoretical foundation, its extendability, its flexible and convenient way to express transformation tasks, its comfortable user interface, and its lean and portable implementation. Ultra itself is written in the functional language Gofer. |

[5] |
W. Guttmann.
Deriving an applicative Heapsort algorithm.
Technical Report UIB-2002-02, Universität Ulm, December 2002.
[ bib |
.html |
http |
.pdf ]
We proceed by program transformation to derive a version of the Heapsort algorithm from a non-deterministic specification. The object language is Haskell and, therefore, the style of the resulting Heapsort program is necessarily applicative. Our development is supported by the program transformation system Ultra. Although a valuable tool, several shortcomings of Ultra are identified. This technical report accompanies [6]. |

[4] |
W. Guttmann, H. Partsch, W. Schulte, and T. Vullinghs.
Tool support for the interactive derivation of formally correct
functional programs (extended abstract).
In D. Haneberg, G. Schellhorn, and W. Reif, editors, FM-TOOLS
2002: The Fifth Workshop on Tools for System Design and Verification, pages
15–20 in Report 2002–11. Institut für Informatik, Universität
Augsburg, June 2002.
[ bib ]
This is a preliminary version of [6]. |

[3] |
W. Guttmann.
Transformationelle Entwicklung des Kerns eines Übersetzers
für eine logische Programmiersprache.
Diplomarbeit, Universität Ulm, October 2001.
[ bib ]
The development of correct programs is desirable for all application areas and necessary for some. In any case it is an intricate task often neglected in favour of efficiency. Compilers, which process programs to speed up their execution, are particularly sensitive. Errors can spread to all translated programs. At the same time, these profit from efficient translation results. This thesis shows the development of a correct compiler that generates efficient results. A characteristic of the logic programs translated by the compiler is that they describe problems instead of specific solution methods. The programmer can therefore focus on the actual task and better perform it. The compiler is developed by program transformation. A program is transformed stepwise into a new program that obtains the same result in a different way. This formal method requires a proof of correctness for such transitions. Particular techniques of transformation developed in this thesis can be clearly distinguished and repeatedly applied. They can be part of a strategy to develop imperative programs from functional specifications. |

[2] |
W. Guttmann.
An Introduction to Ultra.
Universität Ulm, December 2000.
[ bib |
.html |
.pdf ]
This manual provides an introduction to the program transformation system Ultra, sample derivations and a complete system reference. Ultra is based on a dialect of the functional programming language Haskell. |

[1] |
W. Guttmann.
Organisation einer Programmier-Meisterschaft.
Universität Ulm, August 2000.
[ bib ]
This manual describes how to organise a programming contest at a university based on experience with local competitions as part of the ACM ICPC. |