Vasco: Verification and Synthesis of Complex Systems
Members
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.
Publications
The list of publications of VASCO members is available
here.
National and international collaborations
Ongoing projects
Past projects