Dates
3 months : May 1st – July 31st 2021
Georg Struth
Georg Struth studied theoretical physics and philosophy at the University of Heidelberg and obtained a PhD in computer science from the Max Planck Institute for Informatics in Saarbrücken. After a series of positions at German universities he joined the University of Sheffield in 2005.
Laboratories
Uli Fahrenberg, Eric Goubault
Equipe Cosynus
Laboratoire d’informatique ( LIX )
Ecole polytechnique
DigiCosme scientific axe
SciLex
Research interests
• applications of logical and algebraic methods in computer science (axiomatisations, models, completeness, decidability)
• applications of computational methods in mathematics
• concurrency theory, program semantics, probabilistic and hybrid systems
• formalised mathematics with proof assistants
• program verification and correctness (theory and tools)
Main research contributions relevant to DigiCosme proposal
The project has the potential to deliver new algebraic and compositional foundations for concurrent real-time and hybrid systems. It aims at proposing a feasible and realistic solution to the important problem of combining concurrency and real time. The results will be published in a series of journal articles.
Over the last two decades, Georg Struth has made significant contributions to algebraic methods in computer science from foundations (axiomatisations, models, program semantics, completeness, decidability) to application (program verification and transformation, rewriting theory, termination analysis). He is best known for his work on Kleene algebra where he has developed, for instance, modal and concurrent extensions that are instrumental for the project proposed. Georg Struth has also pioneered the development of mathematical and program verification components using such algebras with automated and interactive theorem provers and been instrumental in running the RAMiCS conference series, a platform for research on relational and algebraic methods in computer
science. Building on his background in theoretical physics, has recently designed the first components for the deductive verification of hybrid systems with a proof assistant. The main motivation for this proposal therefore lies in new foundations and tools for real-time and hybrid concurrent and distributed systems. Together with Fahrenberg, Goubault and others, notably Samuel Mimram and Cameron Calk (PhD student) from LIX, Philippe Malbos (Lyon), and Christian Johansen (Oslo), Georg Struth has more recently started a research programme on marrying MKA and CKA with categorical algebra and geometric approaches to concurrency.
The have developed higher-dimensional extensions of modal and concurrent Kleene algebras with languages of polygraphs/computads as models and used them for proving coherence results in higher-dimensional rewriting. They have also worked on algebras supporting the geometric approaches to concurrency developed at LIX, using partial and interval orders, precubical sets and higher-dimensional automata. Further publications are forthcoming this autumn. Beyond this current line of work, Goubault and Fahrenberg, together with Sylvie Putot and Sergio Mover at LIX, have strong interests and track records in real-time and hybrid systems
verification. This opens the door for additional work with Georg Struth within the DigiCosme scheme. Fahrenberg and Goubault are already coordinating an international working group on distributed hybrid systems and the research proposed advances its agenda. It is thus of strategic interest to the group at LIX.
Seminar: Verifying Hybrid Systems with Interactive Theorem Provers
Wednesday 21 April 2021 at 11:00, online seminar
Invited by the Cosynus team.
Course: Kleene Algebras: From Foundations to Program Verification
Teacher: Georg Struth, University of Sheffield, UK
The course will be held online during May, every Friday between 9:00 and 12:00: that is, on the dates of 7, 14, 21, and 28 May.
The course is aimed at M2 and PhD students and everyone else interested and will cover Kleene algebras and extensions plus their implementation in Isabelle/HOL.
Abstract: Kleene algebras were originally proposed as axiom systems for the equational theory of regular expressions. Yet beyond theoretical computer science, they have found their place in computational modelling, in particular program construction and verification. This short course introduces some of the most prominent variants, including Kleene algebras with tests, modal Kleene algebras or concurrent Kleene algebras, and shows how verification components based on these algebras can be built with the Isabelle/HOL proof assistant, introducing this tool along the way.
After a brief historical overview, I introduce Kozen’s axiom system for Kleene algebra, discuss some computationally interesting models and present Kozen’s completeness proof with respect to the equational theory of regular expressions. Then I show how Kleene algebras with tests allow us to model simple while programs and to verify them in algebraic approaches to Hoare logic and Morgan’s refinement calculus. Depending on interest, I may also present modal Kleene algebras, point out connections to dynamic logics and predicate transformer semantics, or introduce concurrent Kleene algebra together with its most important models. Throughout the course, I will use Isabelle to prove algebraic theorems and further to develop simple
prototypical program verification components with very little effort. Yet no previous knowledge of proof assistants is assumed.
The course is divided into six hours of lectures and six hours of exercise sessions. Lecture material and Isabelle theories will be made available before the start of the course.
To register for the course, send an email containing your name and affilation to ulrich.fahrenberg@polytechnique.edu