Pôle Modèles Model Checking and Synthesis

Contact: Laurent Doyen

Overview

We are interested in the foundations of computation. Formal models of computation include classes of languages and machines such as finite automata, games, pushdown and counter systems, weighted automata, (continuous) timed systems, stochastic processes. We identify and study fundamental properties of these models, such as expressiveness, computational complexity, succinctness, equivalence among different models.

We embed our study into rigorous mathematical framework rooted with formal logic, and develop algorithmic procedures, either to prove the correctness of a model, or to provide a counter-example. We develop decision procedures for solving fundamental questions related to the models and logics (satisfiability, realizability, optimization) and provide complexity lower and upper bounds (time and space).

Our goal is to provide efficient techniques and tools to automate and optimize the design of systems (software, circuits, etc.). We seek to establish the correctness of systems through the approaches of verification, diagnosis, learning, control, and synthesis. Furthermore, we develop quantitative approaches to optimize the quality of designed systems.

Members

Permanent

Emeritus

PhD Students

Thomas Soullard

Isa Vialard

PostDoc

Publications

Full list of publications: https://hal.science/LMF-MCS

Recent Publications

  • (), In , (editors), p. , , , , , , , . .
    [URL] [PDF]

Projects

Current

BisoUS

Better Synthesis for Quantitative Underspecified Systems
ANR
2023-2027

MAVeriQ

Méthodes d'Analyse pour la Vérification de propriétés Quantitatives
ANR
2021 - 2025

Narco

Non-Aggregative Resource COmpositions
ANR
2022 - 2026

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

Past

BraVAS

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

Ticktac

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

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