Walter Guttmann
Publications
Please see the main page for contact, research and teaching information.
Journal articles
 An Algebraic Framework for Minimum Spanning Tree Problems, TCS, 2018
 StoneKleene Relation Algebras, AFP, 2017
 An algebraic approach to multirelations and their properties (with R. Berghammer), JLAMP 88:4563, 2017
 A framework for automating security analysis of the Internet of Things (with M. Ge, J. B. Hong, D. S. Kim), JNCA 83:1227, 2017
 Stone Relation Algebras, AFP, 2017
 Stone Algebras, AFP, 2016
 An Algebraic Approach to Computations with Progress, JLAMP 85(4):520539, 2016
 Kleene Algebras with Domain (with V. B. F. Gomes, P. Höfner, G. Struth, T. Weber), AFP, 2016
 Infinite executions of lazy and strict computations, JLAMP 84(3):326340, 2015
 Algebras for Correctness of Sequential Computations, SCP 85(B):224240, 2014
 Multirelations with Infinite Computations, JLAMP 83(2):194211, 2014
 Extended Designs Algebraically, SCP 78(11):20642085, 2013
 Algebras for Iteration and Infinite Computations, Acta Informatica 49(5):343359, 2012
 Typing Theorems of Omega Algebra, JLAP 81(6):643659, 2012
 Fixpoints for General Correctness, JLAP 80(6):248265, 2011
 Imperative Abstractions for Functional Actions, JLAP 79(8):768793, 2010
 Normal Design Algebra (with B. Möller), JLAP 79(2):144173, 2010
 Tool Support for the Interactive Derivation of Formally Correct Functional Programs (with H. Partsch, W. Schulte, T. Vullinghs), J.UCS 9(2):173188, 2003
Conference papers
 Stone relation algebras, RAMiCS 2017
 Relationalgebraic verification of Prim's minimum spanning tree algorithm, ICTAC 2016
 Closure, Properties and Closure Properties of Multirelations (with R. Berghammer), RAMiCS 2015
 A RelationAlgebraic 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 TarskiKleene 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
 Nontermination in Unifying Theories of Programming, RelMiCS/AKA 2005
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
[55] 
W. Guttmann.
An algebraic framework for minimum spanning tree problems.
Theoretical Computer Science, 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 weightedgraph 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].

[54] 
W. Guttmann.
Stonekleene relation algebras.
Archive of Formal Proofs, October 2017.
[ bib 
.html 
.pdf ]
We develop StoneKleene 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 automatabased 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 reflexivetransitive 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 upclosed 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 widescale 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 welldefined 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, relationalgebraic 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 reflexivetransitive closures in semirings.

[49] 
W. Guttmann.
Relationalgebraic 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 weightedgraph 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 pseudocomplemented 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 nontermination. We introduce a model of sequential computations that generalises and abstracts these examples. We generalise existing algebras for nonterminating executions and instantiate these with our model. Using these algebras we derive an approximation order for computations with time and for tracebased 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 upclosed multirelations; this includes connections between various kinds of reflexivetransitive closure.

[44] 
R. Berghammer and W. Guttmann.
A relationalgebraic 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 upclosed 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 upclosed 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 matrixbased models. The models cover nonstrict 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 statebased nondeterministic 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 nonstrict 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 whileloops 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 whileprograms 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 TRCOSC 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 matrixbased computation models. These models support a single kind of nondeterminism, which is either angelic, demonic or erratic with respect to the infinite executions of a computation. Other models, notably isotone predicate transformers or upclosed 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 matrixbased 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 nondeterminism. 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 nonterminating and aborting executions of sequential, nondeterministic 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 nondeterministic choice, sequential composition, whileloops 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 whileprograms. 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 ]
Nonstrict 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 nonstrictness, 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 nonstrict 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 nonsquare 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 1free omega algebras can be transferred to typed omega algebras. This covers every universal 1free 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, prepost 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 semiringbased 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 EgliMilner 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 EgliMilner 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 semiringbased treatments to obtain results about the EgliMilner order.

[30] 
W. Guttmann, G. Struth, and T. Weber.
A repository for TarskiKleene 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 1free omega algebra, typed 1free omega algebra and typed omega algebra. They are based on Kozen's axioms for 1free 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 1free variants. We set up a matrix algebra over typed 1free omega algebras by lifting the underlying structure. The algebra includes nonsquare matrices and care has to be taken to preserve typecorrectness. 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 1free omega algebra into 1free 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 +, ⋅, ^{+}, ^{ω} and 0 carries over from omega algebra to its typed variant. This corresponds to Kozen's result for typed Kleene algebra.

[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 nondeterministic, 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 whileprograms 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 pairbased 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, pairbased 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 nonstrict, 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 divideandconquer. To support program reasoning, we prove laws such as foldmap 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 nonstrict 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 nontermination. 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 whileprograms 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 whileprograms, which is a new result for general correctness and extends to programs with nondeterministic 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 EgliMilner 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 tailrecursion. This substantially involves Kleene and omega algebra as well as additional algebraic formulations of determinacy, invariants, domain, preimage, 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 EgliMilner 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 D8 of Lecture Notes in
Informatics, pages 141–150. Gesellschaft für Informatik, 2008.
[ bib ]
This summary of [17] was invited as it was shortlisted 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 nonstrict computations in an imperative, nondeterministic context. Undefinedness is represented independently of nontermination. 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 nondeterministic, 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 nonstrict 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, preimage, 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 nontermination. Besides being closer to practice, it forms the basis of a new theory of relations representing nonstrict 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 200628, 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 tailrecursion; this substantially involves Kleene and omega algebra as well as additional algebraic formulations of determinacy, invariants, domain, preimage, 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 NPcompleteness. 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 fixedpoint semantics of the demonic while loop that are simpler than the ones obtained from standard UTP theory and previous algebraic approaches.

[11] 
W. Guttmann.
Nontermination 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 UIB200503, 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 NPcompleteness. 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 200515, 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.
Nontermination 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 highlevel descriptive or operational specifications. We illustrate its utility by deriving a version of the Heapsort algorithm from a nondeterministic 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 developmentnavigating 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 UIB200202, Universität Ulm, December 2002.
[ bib 
.html 
http 
.pdf ]
We proceed by program transformation to derive a version of the Heapsort algorithm from a nondeterministic 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, FMTOOLS
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 ProgrammierMeisterschaft.
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.
