Pôle Modèles Model Checking and Synthesis

Responsable: Laurent Doyen

Aperçu

Nous nous intéressons aux fondements des modèles de calcul. Les modèles formels de calcul comprennent les classes de langages et de machines tels que les automates finis, les jeux, les systèmes à piles et à compteurs, les automates pondérés, les systèmes temporisés (continus), les processus stochastiques. Nous identifions et étudions les propriétés fondamentales de ces modèles, telles que l'expressivité, la complexité computationnelle, la concision, l'équivalence entre différents modèles.

Nous intégrons notre étude dans un cadre mathématique rigoureux basé sur la logique formelle, et nous développons des procédures algorithmiques capables soit de prouver la correction d'un modèle, soit de construire un contre-exemple. Nous développons des procédures de décision pour résoudre des questions fondamentales liées aux modèles et aux logiques (satisfiabilité, réalisabilité, optimisation) et nous établissons des limites inférieures et supérieures de complexité (en temps et en espace).

Notre objectif est de proposer des techniques et des outils efficaces pour automatiser et optimiser la conception de systèmes (logiciels, circuits, etc.). Nous cherchons à établir la correction des systèmes par des approches de vérification, de diagnostic, d'apprentissage, de contrôle et de synthèse. De plus, nous développons des approches quantitatives permettant d'optimiser des critères de qualité (temps de réponse, consommation d'énergie, etc.).

Members

Permanent

Emeritus

PhD Students

PostDoc

Raine Rönnholm

Projects

BraVAS

Ideal-based algorithms for VASSes and well-structured systems
ANR
2018-2020

MAVeriQ

ANR
2021 - 2024

Ticktac

Efficient Techniques and Tools for the Verification and Synthesis of Real-Time Systems
ANR
2019-2023

LeaRNNify

New Challenges for Recurrent Neural Networks and Grammatical Inference
CampusFrance & DAAD
Since 2020

IRL Relax

Indo-French Research Lab
Since 2017

IRL SINFIN

Argentino-French Research Lab
Since 2019

DyLo-MPC

Dynamic Logics: Model Theory, Proof Theory and Computational Complexity
STIC-Amsud
2020 - 2021

Keywords

  • Formal models of computation
    • Finite/Infinite
    • Boolean/Quantitative
    • Real-time/Partial information/Stochasticity
    • Games
  • Logic & decision problems
    • Expressiveness
    • Satisfiability/Realizability
    • Satisfiability modulo theories (SMT)
    • Decidability/Complexity
  • Automated system design
    • Tools/prototypes
    • Applications: Software verification, diagnosis, learning, control, synthesis

()
()
.
[URL] [PDF]
()
()
, .