Laboratoire d'informatique de l'École polytechnique

Research at LIX

The Computer Science Laboratory of Ecole Polytechnique (LIX) develops both fundamental and applied research at the best academic level in its 13 teams structured in 5 poles. At the cutting edge of math/CS interactions since its origins, LIX is now also deeply involved in fruitful industrial collaborations and its researchers are fully engaged in societal challenges.

Most of our teams contribute to the transverse thematics Fundations of Computer Science with a particular enphasis on the interactions with mathematics, Quality and Safety of Software and Communications aiming at providing the basis for an efficient, reliable and secure digital world, and Artificial Intelligence, ranging from data science to symbolic approaches through autonomous agent certification.

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

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.