The VERTICS team is part of the Crucial Computing Theme.

The research topics of the VERTICS team are related with critical communicating systems having strong requirements in terms of temporal constraints. The design of such systems consists in defining and realizing software components characterized by strong temporal and cooperative properties. Formal description techniques, relying on mathematical bases, offer automatic verification at the specification level. We are interested in temporal features, efficiency of verification algorithms, and integration of these formal techniques into engineering processes.

Our work focuses on models able to express parallelism, communication, temporal constraints and, more recently, hybrid systems. In order to analyse these models, we design verification algorithms (or semi-algorithms and over-approximations whenever problems are known undecidable). Besides, we also consider the definition of new abstractions (symmetry, partial orders, symbolic representation of set of states, ...) which should avoid combinatorial explosion for larger-scale models.

We have defined so far the FIACRE language, in collaboration with project VASY / CONVECS and the Acadie team (IRIT) within project Topcased of aerospace valley.