The Cosynus team is part of the LIX laboratory at École Polytechnique. Its is to develop techniques in order to model and statically analyze programs and systems, study their invariants, temporal properties, and guarantee their correctness. We mainly focus on two paradigms which are known to be intrinsically difficult to cope with:

  • numerical systems suffer from errors due to the limited numerical precision of computations compared to the mathematical analysis, as well as uncertainties due to the presence of physical elements in hybrid systems (unknown parameters, sensors with limited precision, etc.),

  • concurrent systems can be scheduled in many ways (we cannot predict in advance the relative computation speeds of synchronizations of the computing processes) making the analysis of all the possible behaviors combinatorially very difficult.

The way we address these challenges is by resorting to abstract models for the programs and the data they handle, on which we can use tools developed in theoretical computer science, as well as in applied and pure mathematics. Most notably, many of the works of the team are based on the following methods:

  • abstract interpretation is the main technique used in order to symbolically evaluate programs, in particular domains based on affine forms have been used and developed intensively in order to compute the evolution of hybrid systems,

  • geometric methods coming from algebraic topology (homotopy, homology, etc.) are adapted in order to be applicable to the models of computer programs and provide new families of invariants.

More recently, the study of the interplay between algebraic and geometric structures encountered in topological models of computer programs has motivated a series of more theoretical work on

  • higher-dimensional categories, which are algebraic structures playing a central role in modern algebraic topology.

The team, which has a strong focus on theory, tries when possible to develop the techniques down to the point where concrete applicability can be demonstrated, by implementing prototypes and conducting benchmarks (see our GitHub page).