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.
Page mise à jour le 17/09/2013 à 13:32