Modeling and Verification
Head: Marc Zeitoun.
General presentation
The research theme Modeling and Verification (MV) continues research
initiated in the early eighties by the group MVTsi (led by André Arnold). The members of the
group work on modeling and verification of complex
systems. They develop formal methods for establishing correctness of
systems. The group works on a mix of three types of
activities:
- Theory: design and study of various formalism for
modeling critical systems and expressing their properties: infinite-state and reactive systems,
in particular concurrent, timed and probabilistic systems.
- Algorithmic activity: developing tools for analyzing critical
systems, such as model-checkers and simulators. This activity ranges from
design of algorithms to implementation.
- Modeling activity: modeling real systems in cooperation with
industry. For a long time limited to finite state models (cf. Altarica), this
activity now expands to infinite state models, either discrete or
continuous.
Seminar
Tools
- AltaRica: language and tools for modelling and verification.
- FASTer: a tool dedicated to the analysis of infinite systems.
- Insight: binary program analysis framework.
Projects
- SAFE, projet UE, 2011--.
- VACSIM (Validation de la commande des systèmes critiques par couplage simulation et méthodes d'analyse formelle), ANR 2011-2015.
- MARSHAL, projet FUI (Fonds Unique Interministériel), 2012-2014.
- REACHARD (Taming Hard Reachability Problems for Counter Systems), ANR BLANC (SIMI 2), 2011-2014.
- FREC (Frontiers of recognizability), ANR BLANC, 2010-2013.
- GAMES (Games for Design and Verification) ESF Research Networking Programme, 2008-2012.
- BINCOA (Symbolic Methods for BINary Code Analysis), ANR ARPEGE, 2009-2012.
- AVeriSS (Automated Verification of Software Systems), ANR "Sécurité et Informatique", 2007-2010.
- DocFlow (Analysis, monitoring and optimisation of Web documents and services), ANR "Masse de Données et Connaissances Ambiantes" 2007-2009.
- DOTS (Distributed Open and Timed Systems), ANR "Sécurité et Informatique" 2007--2010.
- SPaCIFY (Ingénierie des modèles et méthodes formelles intégrées pour le développement des logiciels de vol spatiaux), ANR "Technologies logicielles", 2007-2009.
- GAMES (Games for Design and Verification) ESF Research Networking Programme, 2008-2012.
- BINCOA (Symbolic Methods for BINary Code Analysis), ANR ARPEGE, 2009-2011.