Dates
3 mois : 1er mai – 31 juillet 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.
Laboratoires
Uli Fahrenberg, Eric Goubault
Equipe Cosynus
Laboratoire d’informatique ( LIX )
Ecole polytechnique
Axe scientifique DigiCosme
SciLex
Intérêts de recherche
• 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)
Principales contributions de recherche pertinentes pour DigiCosme
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.
Séminaire: Verifying Hybrid Systems with Interactive Theorem Provers
Mercredi 21 avril 2021 à 11:00, en ligne
Invité par l’équipe Cosynus.
Cours: Algèbres de Kleene: des fondements à la vérification des programmes
Professeur: 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.
Résumé: Les algèbres de Kleene ont été proposées initialement comme systèmes axiomatiques pour la théorie equationnelle des expressions régulières. Mais au-delà de l’informatique théorique, elles ont trouvé leur place comme modèles de systèmes informatiques et notamment dans la construction et vérification des programmes. Ce cours compact introduit des variantes bien connues comme les algèbres de Kleene avec tests, les algèbres de Kleene avec domaine ou des algèbres de Kleene concourantes, et explique comment on peut utiliser l’assistant de preuve Isabelle/HOL pour construire des composants de vérification.
Après un bref aperçu historique, j’introduirai le système axiomatique de Kozen et quelques modèles parmi les plus importants, et je présenterai la preuve de complétude de Kozen par rapport aux expressions régulières. J’expliquerai également comment les algèbres de Kleene avec tests donnent une sémantique simple pour les programmes avec boucles et permettent de vérifier leur correction avec des variantes algébriques de la logique de Hoare et le calcul de raffinement de Morgan. Selon l’intérêt, je présenterai les algèbres de Kleene modales et leurs relations aux logiques dynamiques et aux transformateurs de prédicat ou, comme alternative, les algèbres de
Kleene concourantes et leurs modèles d’ordre partiel. En parallèle, j’utiliserai Isabelle pour vérifier des théorèmes algébriques et développer des prototypes simples des composants de vérification avec très peu d’effort. Mais je ne suppose aucune expérience préalable avec un assistant de preuve.
Le cours est composé de six heures de cours et six heures de séance d’exercices. Je fournirai du matériel de cours et des théories déjà programmées en Isabelle.
To register for the course, send an email containing your name and affilation to ulrich.fahrenberg@polytechnique.edu