Journées Systèmes Infinis
10-11 mars 2005 - Cachan
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" :
-
Olivier Serre
(LIAFA, Paris 7, France & RTWH Aachen, Allemagne)
Jeux infinis
-
Christel Baier
(Univ. Bonn, Allemagne)
The Verification of Probabilistic Timed Systems
-
Anca Muscholl
(LIAFA, Paris 7, France)
Asychronously Communicating Systems
-
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 :
-
Helmut Seidl
(TU Munich, Allemagne)
Analyzing Modular Arithmetic
-
Javier Esparza
(Univ. Stuttgart, Allemagne)
Verification of probabilistic procedural programs
-
Antoine Miné
(LIENS, Paris, France)
Weakly relational abstract domains and the efficient inference of
numerical properties in large and infinite systems
-
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 :
-
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
-
Ahmed Bouajjani (LIAFA, Paris 7)
-
Alain Finkel (LSV, ENS de Cachan)
-
Denis Lugiez (LIF, Université de Provence)
-
Philippe Schnoebelen (LSV, ENS de Cachan)
Inscription
-
Montant :
Les frais d'inscription sont de 80 euros TTC, soit 66,89 euros HT + 13,11
euros de TVA. Ils couvrent les déjeuners du 10 et
du 11, le dîner du 10 mars, et les pauses cafés.
-
Inscription :
Compléter le bulletin
d'inscription
(format .pdf ou
format .doc)
et renvoyer le
-
par mail à jsi2005@lsv.ens-cachan.fr
ou par fax au 0147407521
pour le jeudi 3 mars au plus tard,
-
par courrier avec votre réglement
ou votre bon de commande
à l'adresse indiquée sur le bulletin d'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.