Laboratoire d'informatique de l'École polytechnique

Personal musings on semantic models and verification of programs, hybrid, concurrent and distributed systems, by Eric Goubault (Cosynus team)

Location: https://cisco.webex.com/cisco/j.php?MTID=me3bf13b6e414da654a0266fd6b9a7d2f
Date: Thu, 20 May 2021, 13:00-14:00

In semantics and verification, the end justifies any means. Applying this old saying to the letter, program and systems modeling and verification have produced an enormous amount of carefully crafted mathematics over the last 50 years or so. Being approximately of the same age, it seemed like a good idea for me to try to describe some of the methods I have participated in developing, within the Cosynus group at LIX, based on both numerical and symbolic methods and their interplay. On the numerical mathematics side, I will describe some of the abstract interpretation/set-based methods we designed; on the symbolic side of things, I will pick up a few examples of algebraic (mostly categorical and higher-categorical), logical (varieties of temporal and epistemic logics) and geometric (invariants of topological and directed topological spaces). These are in fact all inter-related when you take the right categorical perspective, but this may well go too far for a general presentation. These mathematics constitute a Swiss Army knife for dealing with a varieties of applications: checking control systems (for drones and swarms of drones), possibly including learning-based components (neural networks for perception and control), solving computability and complexity problems for diverse models of computation (rewriting systems, distributed systems etc.) and control and motion planning algorithms, expressing correctness for concurrent data structures etc. If time permits, I will direct the audience to some of these applications whenever possible.