CONVECS Research team

Construction of verified concurrent systems

Team presentation

CONVECS is a research team working on the formal modeling and verification of asynchronous concurrent systems, which are instantiated in various domains (communication protocols, distributed algorithms, Globally Asynchronous Locally Synchronous systems - GALS, etc.). To this aim, CONVECS proposes new formal languages for specifying the behaviour and the properties of concurrent systems, and devises efficient verification algorithms and tools running on sequential and massively parallel machines.

Research themes

Asynchronous concurrency is becoming ubiquitous, from the micro scale of embedded systems (asynchronous logic, network-on-chip, GALS, multi-core processors, etc.) to the macro scale of grids and cloud computing. In the race for improved performance and lower power consumption, hardware architects are moving towards asynchrony, in which several entities operate concurrently without a central clock. The price to pay for enhanced performance is an increased design complexity, which can only be addressed by formal verification.

To improve the state-of-the-art in the design and analysis of concurrent asynchronous systems, CONVECS follows a research programme of five interrelated scientific topics:
  1. Going from high-level formal languages to concurrent implementations.
  2. Parallel and distributed verification algorithms.
  3. Handling of timed, probabilistic, and stochastic aspects.
  4. Component-based architectures for on-the-fly verification.
  5. Real-world applications and case-studies.

International and industrial relations

The CONVECS team is involved in several international working groups in the domain of formal methods and verification:
  • FMICS ERCIM Working Group on Formal Methods for Industrial Critical Systems
  • IFIP Working Group 1.8 on Concurrency Theory
  • AVACS consortium on Automatic Verification and Analysis of Complex Systems
    (involvement of Hubert Garavel in cooperation with Saarland University)
The members of CONVECS develop and maintain the CADP toolbox, a state-of-the-art verification environment for concurrent asynchronous systems. CADP is widely used in both industry and academia. CONVECS collaborates with several industrial partners interested in formal verification, such as Orange Labs, Schneider Electric, and STMicroelectronics.

Keywords: Formal methods; model checking; process algebra; temporal logic; parallel and distributed verification

Research teams of the same theme :

Inria Headquarters and research centres

Direct links

Social