Séjour long

Georg
STRUTH

Sciences Informatique - Royaume Uni

Thèmes de recherche

PROJET

Cohérence algébrique, algèbres de Kleene de dimension supérieure et preuves
interactives

Développées initialement pour modeler des systèmes informatiques, les algèbres de Kleene ont été généralisées récemment pour décrire des systèmes de réécriture de dimension supérieure en mathématiques. Ce projet vise à développer de nouvelles variantes de ces algèbres pour vérifier des propriétés de cohérence en algèbre catégorique. Pour cela il semble essentiel de formaliser cette approche avec des assistants de preuve pour apprivoiser la complexité des preuves dans les catégories supérieures. Le projet souligne particulièrement l’usage de ces algèbres dans le cadre des méthodes géométriques pour les systèmes informatiques concurrents et distribués. Du point de vu opérationnel, les algèbres visent à fournir une couche d’abstraction soutenant des preuves équationnelles avec des diagrammes catégoriques, des stratégies de réduction, et ainsi des preuves automatisées et un traitement algorithmique.

Les résultats envisagés seront par conséquent des nouvelles algèbres de Kleene de dimension supérieure (globulaires, (pré)cubiques et simpliciales), des preuves de cohérence pour les algèbres de dimension supérieure, la formalisation de l’approche avec un assistant de preuve de type Coq ou Isabelle, et son usage dans la concurrence, notamment avec des automates de dimension supérieure.

Activités / CV

BIOGRAPHIE

Georg Struth est professeur en informatique théorique à l’Université de Sheffield, Royaume Uni, et directeur de son laboratoire de vérification. Il a une longue expèrience en recherche sur les algèbres et logiques de programmes, leurs sémantiques, les méthodes de vérification et la formalisation des théories mathématiques avec des assistants de preuve.
Il est surtout connu pour son travail pionnier sur la théorie et les applications des algèbres de Kleene et des quantales, développant des variantes modales, variantes cylindriques, questions relatives à l'exhaustivité et à la décidabilité dans l'application aux programmes et la conception d'outils de vérification.
Son travail plus récent porte sur la vérification quantitative, la sémantique des systèmes probabilistes et hybrides (systèmes dynamiques interagissant avec des systèmes de contrôle discrets), les modèles géométriques de concurrence et de distribution utilisant la réécriture de dimension supérieure des polygraphes et les automates de dimension supérieure.

BIBLIOGRAPHIE

  1. G. Struth Trimming the Hedges: An Algebra to Tame Concurrency, in C.Jones and J. Misra, Theory of Programming: Life and Work of Tony Hoare,Turing Award Series, Association of Computing Machinery, 2021.
  2. B. Dongol, I. J. Hayes and G. Struth. Convolution Algebras: Relational Convolution, Generalised Modalities and Incidence Algebras, Logical Methods in Computer Science 17(1), 2021.
  3. J. Huerta y Munive and G. Struth. Verifying Hybrid Systems with Modal Kleene Algebra. RAMiCS 2018, volume 11194 of LNCS, pages 225–243, Springer, 2018.
  4. A. Armstrong, V. B. F. Gomes and G. Struth . Building Program Construction and Verification Tools from Algebraic Principles, Formal Aspects of Computing, 28(2): 265–293, 2016.
  5. H. Furusawa and G. Struth. Concurrent Dynamic Algebra, ACM Transactions on Computational Logic, 16(4): 30, 2015.
  6. M. R. Laurence and G. Struth. Completeness Theorems for Bi-Kleene Algebras and Series-Parallel Rational Pomset Languages. RAMiCS 2014, volume 8428 of LNCS, pages 65–82, Springer, 2014.
  7. C. A. R. Hoare, B. Möller, G. Struth and I. Wehrman. Concurrent Kleene Algebra and its Foundations, Journal of Logic and Algebraic Programming 80(6):266–296, 2011.
  8. J. Desharnais and G. Struth. Internal Axioms for Domain Semirings, Science of Computer Programming 76(3):181–203, 2011.
  9. C. A. R. Hoare, A. Hussain, B. Möller, P. W. O’Hearn, R. L. Peterson and G. Struth. On Locality and the Exchange Law for Concurrent Processes. CONCUR 2011, volume 6901 of LNCS, pages 250–264. Springer, 2011.
  10. J. Desharnais, B. Möller, and G. Struth. Kleene algebra with domain. ACM Transactions on Computational Logic, 7(4):798–833, 2006.