Keywords: relation algebra, verification, graph algorithms, proof mechanisation
Units: 12/24 units
Background
Relations are among the most ubiquitous concepts in mathematics and computing. Relational calculi have their origin in the late nineteenth century and their initial development was strongly influenced, but then overshadowed, by the advancement of mathematical logic. Around 1940, Alfred Tarski revived the subject by formalising the calculus of binary relations alternatively within the three-variable fragment of first-order logic and as an abstract relation algebra within first-order equational logic Today, relation algebras form an estab- lished field of mathematics with numerous textbooks and research publications.
The relevance of relational calculi in computing has been realised since the early beginnings. Relational approaches had considerable impact on program semantics, refinement and verification through the work of Dijkstra, Hoare, Scott, de Bakker, Back and others. Formal methods like Alloy, B and Z, or Bird and de Moor’s algebraic approach to functional program development are strongly relational. Further applications of relations in computing include data bases, graphs, preference modelling, modal reasoning, linguistics, hardware verification and the design of algorithms. Here, our main motivation is program development and verification.
Research Questions and Tasks
Algorithmic Graph Theory —as taught in many university courses— focuses on the notions of acyclicity and strongly connected components of a graph and the related search algorithms. Our aim is about combining mathematical precision and concision in the context of algorithmic graph theory. Specifically, we use point-free reasoningg about paths in graphs (as opposed to pointwise reasoning about paths between nodes in graphs), resorting to pointwise reasoning only where this is unavoidable.
The aim is to use relation algebra as the basis of a machine-supported formal verification of graph algorithms in order to assess the current state of automated verification systems.
References
-
[BFGH20]
R. Berghammer, H. Furusawa, W. Guttmann & P. Höfner (2020): Relational Characterisations of Paths. Journal of Logic and Algebraic Methods in Programming. Preprint at abs/1801.04026.
-
[BDGW19]
R. Backhouse, H. Doornbos, R. Glück &J. van der Woude (2019): Elements of Algorithmic Graph Theory — An Exercise in Point-Free Reasoning (Working Document). Available at www.cs.nott.ac.uk/~psarb2/MPC/BasicGraphTheory.pdf.
Requirements: interest in logic and algebraic reasoning, some experience with interactive theorem provers such as Isabelle/HOL, Coq or HOL is of advantag