CONVECS Research team
Construction of verified concurrent systems
- Leader : Radu Mateescu
- Type : Project team
- Research center(s) : Grenoble
- Field : Algorithmics, Programming, Software and Architecture
- Theme : Proofs and Verification
- Partner(s) : Institut polytechnique de Grenoble,Université Joseph Fourier (Grenoble)
- Collaborator(s) : Laboratoire d'Informatique de Grenoble (LIG) (UMR5217)
Team presentationCONVECS 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, cloud computing, 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 machines and distributed infrastructures.
Research themesAsynchronous concurrency is becoming ubiquitous, from the micro scale of embedded systems and multi-core processors to the macro scale of grids and cloud computing. In the race for improved performance and lower power consumption, computer manufacturers are moving towards asynchrony, in which several entities operate concurrently at different speeds, communicate and synchronize. 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:
- Going from high-level formal languages to concurrent implementations.
- Parallel and distributed verification algorithms.
- Handling of timed, probabilistic, and stochastic aspects.
- Component-based architectures for on-the-fly verification.
- Real-world applications and case-studies.
International and industrial relationsThe 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)
Research teams of the same theme :
- ANTIQUE - Static Analysis by Abstract Interpretation
- CELTIQUE - Software certification with semantic analysis
- DEDUCTEAM - DEDUCTEAM
- GALLINETTE - Gallinette: developing a new generation of proof assistants
- GALLIUM - Programming languages, types, compilation and proofs
- MARELLE - Mathematical, Reasoning and Software
- MEXICO - Modeling and Exploitation of Interaction and Concurrency
- MOCQUA - Designing the Future of Computational Models
- PARSIFAL - Proof search and reasoning with logic specifications
- PI.R2 - Design, study and implementation of languages for proofs and programs
- SUMO - SUpervision of large MOdular and distributed systems
- TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
- VERIDIS - Modeling and Verification of Distributed Algorithms and Systems