2014 | VERICONISS

Verification of Concurrent Infinite State Systems 

Axe :SciLex
Sujet : reachability, model checking and equivalence checking of concurrent infinite state systems
Coordinateur : Stefan Göller
Equipe:

  • P1: Laboratoire Spécification et Vérification in Cachan (France) – Alain Finkel, Stéphane Demri, Sylvain Schmitz, Philippe Schnoebelen, Stefan Schwoon)
  • P2: Laboratoire d‘Informatique Algorithmique: Fondaments et Applications in Paris (France – (Peter Habermehl, Olivier Serre)
  • P3: Laboratoire d‘Informatique de l‘Institut Gaspard Monge in Marne-La-Vallée (France (Arnaud Carayol)
  • P4: Laboratoire Bordelais de Recherche en Informatique in Bordeaux (France)-(Jérôme Leroux, Géraud Sénizergues, Grégoire Sutre)
  • P5: Max-Planck Institute for Software Systems (MPI-SWS) in Kaiserslautern (Germany)- Dmitry Chistikov, Rupak Majumdar)
  • P6: Department of Computer Science at Technical University of Ostrava (Czech Republic)- Stanislav Böhm, Petr Jancar)

Candidats: Georg Zetzsche (Post-doc), Christoph Haase (Post-doc), Piotr Hofman (Post-doc)
Laboratoire : LSV Cachan
Durée du projet : 2014/2017

Introduction
Ce projet de recherche vise à étudier les questions centrales de la recherche sur l’accessibilité, la vérification des modèles et la vérification de l’équivalence des modèles de systèmes à états infinis qui permettent de modéliser la concurrence. Ce domaine de recherche est jeune et actif d’une part, mais aussi complexe et très mal compris d’autre part. Notre objectif est de mieux comprendre le comportement algorithmique des systèmes à états infinis simultanés en ce qui concerne les tâches de vérification formelle mentionnées ci-dessus.

D’une manière très générale, nous aimerions répondre aux questions suivantes. Premièrement, quand la tâche de vérification respective est-elle décidable, c’est-à-dire quand peut-elle être résolue efficacement sur ordinateur ? Deuxièmement, dans le cas où la tâche de vérification respective est décidable, combien de ressources en termes de temps et d’espace sont suffisantes et nécessaires pour la résoudre sur ordinateur ?

Documents:

Publications

Projet transverse :