
R.J. van Glabbeek, P. Höfner, R. Horne:
Assuming Just Enough Fairness to make Session Types Complete for Lockfreedom. In Logic in Computer Science (LICS 2021). IEEE, 2021.
arXiv: CoRR abs/2104.14226
abstract  pdf  bibtex
Abstract:
We investigate how different fairness assumptions affect results concerning lockfreedom, a typical liveness property targeted by session type systems. We fix a minimal session calculus and systematically take into account all known fairness assumptions, thereby identifying precisely three interesting and semantically distinct notions of lockfreedom, all of which having a sound session type system. We then show that, by using a general merge operator in an otherwise standard approach to global session types, we obtain a session type system complete for the strongest amongst those notions of lockfreedom, which assumes only justness of execution paths, a minimal fairness assumption for concurrent systems.
@InProceedings{Hoefner20213,
Author = {van Glabbeek, R.J. and H{\"o}fner, P. and Horne, R.},
Title = {Assuming Just Enough Fairness to make Session Types Complete for Lockfreedom},
BookTitle = {Logic in Computer Science (LICS 2021)},
Editor = {},
Series = {},
Volume = {0},
Pages = {},
Year = {2021},
Publisher = {IEEE},
Doi = {}
}

R. Bird, J. Gibbons, R. Hinze, P. Höfner, J. Jeuring, L. Meertens, B. Möller, C. Morgan, T. Schrijvers, W. Swierstra, N. Wu:
Algorithmics. In IFIP Advances in Information and Communication Technology, Springer, 0. (accepted)
abstract  pdf  bibtex
Abstract:
Algorithmics is the study and practice of taking a highlevel description of a program's purpose and, from it, producing an executable program of acceptable efficiency. Each step in that process is justified by rigorous, careful reasoning at the moment it is taken; and the repertoire of steps allowed by that rigour, at each stage, guides the development of the algorithm itself. IFIP's Working Group 2.1 has always been concerned with Algorithmics: both the design of its notations and the laws that enable its calculations. Even ALGOL 60 showed that orthogonality, simplicity and rigour in a programming language improves the quality of its programs. Our Group's title ``Algorithmic Languages and Calculi'' describes our activities: the discovery of precise but more general rules of calculational reasoning for the many new styles of programming that have developed over the 60 years since IFIPâ€™s founding. As our contribution to the birth day celebrations, we outline how we have tried to contribute during those decades to the rigorous and reliable design of computer programs of all kinds  to Algorithmics.
@article{Hoefner20212,
Author = {Bird, R. and Gibbons, J. and Hinze, R. and H{\"o}fner, P. and Jeuring, J. and Meertens, L. and M{\"o}ller, B. and Morgan, C. and Schrijvers, T. and Swierstra, W. and Wu, N.},
Title = {Algorithmics},
Journal = {IFIP Advances in Information and Communication Technology},
Year = {0},
Publisher = {Springer},
}

R. Berghammer, H. Hitoshi, W. Guttmann, P. Höfner:
Relational Characterisations of Paths. In Journal of Logic and Algebraic Methods in Programming 117, Elsevier, 2020.
arXiv: CoRR abs/1801.04026  doi: 10.1016/j.jlamp.2020.100590
abstract  pdf  bibtex
Abstract:
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 pointwise reasoning when it comes to arguments about paths in a graph. We present a purely algebraic way to specify different kinds of paths in relation algebras. We study the relationship between paths with a designated root vertex and paths without such a vertex. Since we stay in firstorder 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 Isabelle/HOL.
@article{Hoefner20203,
Author = {Berghammer, R. and Hitoshi, H. and Guttmann, W. and H{\"o}fner, P.},
Title = {Relational Characterisations of Paths},
Journal = {Journal of Logic and Algebraic Methods in Programming},
Volume = {117},
Year = {2020},
Publisher = {Elsevier},
Doi = {10.1016/j.jlamp.2020.100590}
}

J. Drury, P. Höfner, W. Wang:
Formal Models of the OSPF Routing Protocol. In A. Fehnker, H. Garaval (eds.), Models for Formal Analysis of Real Systems (MARS 2020). Electronic Proceedings in Theoretical Computer Science 316, pp. 72120, Open Publishing Association, 2020.
doi: 10.4204/EPTCS.316.4
abstract  pdf  bibtex
Abstract:
We present three formal models of the OSPF routing protocol. The first two are formalised in the timed process algebra TAWN, which is not only tailored for routing protocols, but also specifies protocols in pseudocode that is easily readable. The difference between the two models lies in the level of detail (level of abstraction). From the more abstract model we then generate the third model. It is based on networks of timed automata and can be executed in the model checker Uppaal.
@InProceedings{Hoefner20202,
Author = {Drury, J. and H{\"o}fner, P. and Wang, W.},
Title = {Formal Models of the {OSPF} Routing Protocol},
BookTitle = {Models for Formal Analysis of Real Systems (MARS 2020)},
Editor = {Fehnker, A. and Garaval, H.},
Series = {Electronic Proceedings in Theoretical Computer Science},
Volume = {316},
Pages = {72120},
Year = {2020},
Publisher = {Open Publishing Association},
Doi = {10.4204/EPTCS.316.4}
}

R. Barry, R.J. van Glabbeek, P. Höfner:
Formalising the Optimised Link State Routing Protocol. In A. Fehnker, H. Garaval (eds.), Models for Formal Analysis of Real Systems (MARS 2020). Electronic Proceedings in Theoretical Computer Science 316, pp. 4071, Open Publishing Association, 2020.
doi: 10.4204/EPTCS.316.3
abstract  pdf  bibtex
Abstract:
Routing protocol specifications are traditionally written in plain English. Often this yields ambiguities, inaccuracies or even contradictions. Formal methods techniques, such as process algebras, avoid these problems, thus leading to more precise and verifiable descriptions of protocols. In this paper we use the timed process algebra TAWN for modelling the Optimised Link State Routing protocol (OLSR) version 2.
@InProceedings{Hoefner20201,
Author = {Barry, R. and van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {Formalising the Optimised Link State Routing Protocol},
BookTitle = {Models for Formal Analysis of Real Systems (MARS 2020)},
Editor = {Fehnker, A. and Garaval, H.},
Series = {Electronic Proceedings in Theoretical Computer Science},
Volume = {316},
Pages = {4071},
Year = {2020},
Publisher = {Open Publishing Association},
Doi = {10.4204/EPTCS.316.3}
}