Vasco: Verification and Synthesis of Complex Systems


Permanent Members

Dietmar Berwanger
Researcher, CNRS
Benedikt Bollig
Senior researcher, CNRS
Patricia Bouyer-Decitre
Senior researcher, CNRS
Laurent Doyen
Researcher, CNRS
Laurent Fribourg
Senior researcher, CNRS
Paul Gastin
Professor, ENS Paris-Saclay
Stéphane Le Roux
Assistant professor, ENS Paris-Saclay

Ph.D. Students

Mauricio Gonzãlez
PhD student, ERC EQualIS
Mathieu Hilaire
PhD student
Jawher Jerray
PhD student (joint with LIPN, funded by Paris 13)
Anirban Majumdar
PhD student
Adnane Saoud
PhD student (joint with L2S, funded by Digicosme Emergence Codecsys)
Olivier Stietel
PhD student (joint with IRIF, funded by ANR FREDDA)
Nathan Thomasset
PhD student
Pierre Vandenhove
PhD student (joint with UMONS, Belgium)

Research topics

The VASCO team is concerned with the automated verification, synthesis, and inference of complex systems. The term complex refers to characteristics that one often encounters in safety-critical applications, such as quantitative constraints and intricate interactions between (controllable or uncontrollable) components in a distributed system. We develop formal models and efficient algorithms to verify, optimize, synthesize, and infer complex systems. Below, we present some concrete research objectives:

Game-Based Synthesis and Control of Complex Systems

Synthesis and control problems can often be understood as the computation of winning strategies in games where antagonistic players represent the system and an uncontrollable environment. Though game-theoretic foundations of computer systems have recently seen major advances, many questions remain unanswered when quantitative requirements specifications come into play (such as resource limitations or robustness constraints), or multiple players or components are interacting. As those features are an indispensable part of modern computational devices, we aim to develop their game-theoretic foundations.

New Challenges for Recurrent Neural Networks and Grammatical Inference

There is a growing need for verifying and validating machine-learning algorithms in various application domains such as intelligent medical diagnostics, autonomous vehicles, natural-language processing, etc. Recurrent neural networks (RNNs) are a state-of-the-art machine-learning tool for processing and classifying sequential data. Our aim is to employ formal methods and, in particular, grammatical inference and automata learning, to enhance the understanding of RNNs. We are also exploring the use of RNNs in the process of verifying reactive systems.


The list of publications of VASCO members is available here.

National and international collaborations

Ongoing projects

Past projects

About LSV