Journées Systèmes Infinis
10-11 mars 2005 - Cachan

Quelques photos de l'événement !

Sommaire

Vérification des Systèmes Infinis

La vérification des systèmes infinis est un domaine de recherche actif qui attire des chercheurs de différentes communautés. En effet, la vérification de systèmes complexes, aussi bien logiciels que matériels, doit tenir compte d'aspects qui sont hors de portée des techniques et outils basés sur l'analyse de modèles finis (model-checking). Parmi ces aspects, l'on peut citer: la manipulation de variables et de structures de données non bornées (compteurs, horloges, files d'attentes, tableaux), la paramétrisation (protocoles et algorithmes distribués avec un nombre arbitraire de composants), la mobilité et le dynamisme, la sécurité, etc.

Le problème de la vérification des systèmes infinis est actuellement abordé selon plusieurs approches basées sur différentes techniques: abstraction, analyse symbolique d'accessibilité, etc., et utilisant différents outils mathématiques: théories des langages et automates, logiques, systèmes de réécriture, résolution de contraintes, etc.

But des JSI

Le but des Journées Systèmes Infinis est d'offrir aux chercheurs et aux doctorants l'occasion de se rencontrer, de croiser leurs expériences, de se tenir au courant de l'état de l'art et de découvrir les nouvelles applications, et de reconnaître les axes de recherches futurs concernant les systèmes infinis et les problèmes liés à leur analyse.

Les journées JSI 2005 viennent à la suite des précédentes Journées Systèmes Infinis organisées à Cachan en 1998, à Paris en 2001, à Luminy en 2002, à Grenoble en 2003.

Programme scientifique

Le programme des journées JSI 2005 était composé de quatre exposés de type "survey" :
  1. Olivier Serre (LIAFA, Paris 7, France & RTWH Aachen, Allemagne)
    Jeux infinis
  2. Christel Baier (Univ. Bonn, Allemagne)
    The Verification of Probabilistic Timed Systems
  3. Anca Muscholl (LIAFA, Paris 7, France)
    Asychronously Communicating Systems
  4. Patricia Bouyer (LSV, ENS de Cachan, France)
    Automates temporisés et extensions : frontières de la décidabilité
de quatre exposés techniques présentant des résultats récents :
  1. Helmut Seidl (TU Munich, Allemagne)
    Analyzing Modular Arithmetic
  2. Javier Esparza (Univ. Stuttgart, Allemagne)
    Verification of probabilistic procedural programs
  3. Antoine Miné (LIENS, Paris, France)
    Weakly relational abstract domains and the efficient inference of numerical properties in large and infinite systems
  4. S. Bardin (LSV, ENS de Cachan, France)
    Flat Acceleration: the Theory Behind FAST
et d'un groupe de travail de plus longue durée où a été présentée en détail une construction efficace pour l'extraction de formules de Presburger à partir d'automates binaires :
  1. Jérôme Leroux (IRISA, Rennes, France)
    De l'automate binaire à la formule de Presburger

Lieu - Horaires

Lieu : ENS de Cachan (comment y accéder),
Bâtiment d'Alembert,
Salle Condorcet (montez un étage depuis l'entrée principale).

Jeudi 10 mars 2005

Vendredi 11 mars 2005

Comité d'organisation

  1. Ahmed Bouajjani (LIAFA, Paris 7)
  2. Alain Finkel (LSV, ENS de Cachan)
  3. Denis Lugiez (LIF, Université de Provence)
  4. Philippe Schnoebelen (LSV, ENS de Cachan)

Inscription

Une liste d'hôtels

Pour pouvoir se rendre facilement à l'ENS de Cachan (cf. plan d'accès) il est pratique de trouver un hébergement proche de la ligne du RER B. Vous trouverez quelques possibilités sur le site de l'ENS de Cachan.

À propos du LSV