Jean-Michel COUVREUR, LIFO, Université d'Orléans (couvreur@univ-orleans.fr)
Olga KOUCHNARENKO, LIFC, Université de Franche-Comté (kouchna@lifc.univ-fcomte.fr)
L'action proposée ici est la mise à jour de l'action SLOVO (Sémantiques Logique et Opérationnelles, Vérification et Optimisation) engagée lors de la précédente campagne. Rappelons que SLOVO fut un groupe de travail visant des applications dans les domaines de ``spécification-test-preuve'' du GDR-ALP, et d'``algorithmique'' du GDR-ARP pour l'optimisation par la parallélisation, et centré sur des travaux dans les domaines de la démonstration automatique et de la programmation logique.
La mise à jour de l'action SLOVO - avec un nouveau sigle - répond à un souci de mieux refléter l'évolution de nos directions de recherche actuelles dans les domaines de la spécification et de la vérification de systèmes. Notre objectif principal est l'élaboration d'outils et de méthodes pour la vérification de protocoles de sécurité, de services web, de systèmes embarqués et pour l'analyse de documents semi-structurés.
Les principaux thèmes abordés dans le projet FORWAL sont :
- Formalismes à base d'automates (de mots et d'arbres) et de contraintes pour la vérification de protocoles de sécurité, de services web et de systèmes embarqués
- Langage d'arbres et de DAG pour l'analyse de documents semi-structurés
- Calcul symbolique à base d'automates pour la vérification de systèmes à variables hétérogènes
- Langage (non régulier) d'arbres et vérification de protocoles de sécurité et services web
- Vérification par des techniques ordre partiel et logique de la concurence
- Validation de protocoles par l'approche inductive
La participation aux activités du groupe FORWAL est naturellement ouverte à tous les chercheurs dont les domaines de travaux sont proches, quel que soit leur GDR de rattachement (comme ce fut le cas déjà avec SLOVO).
PRV - Laboratoire d'Informatique Fondamentale d'Orléans (LIFO) - Orléans
TFC - Laboratoire d'Informatique de l'Université de Franche-Comté (LIFC) - Besançon
CASSIS, PROTHEO - Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA) - Nancy
LANDE, S4 - Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA) - Rennes
SRC - Laboratoire d'Informatique de Paris 6 (LIP6) - Paris
MVTsi - Laboratoire Bordelais de Recherche en Informatique (LaBRI) - BordeauxParticipants principaux
Siva Anantharaman (LIFO, Orléans), Fabrice Bouquet (LIFC, Besançon), Gérard Cécé (LIFC, Besançon), Jean-Michel Couvreur (LIFO, Orléans), Thomas Genet (IRISA, Rennes), Alain Giorgetti (LIFC, Besançon), Pierre-Cyrille Héam (LIFC, Besançon), Olga Kouchnarenko (LIFC, Besançon), Jérome Leroux (LaBRI, Bordeaux), Sébastien Limet (LIFO, Orléans), Pierre-Etienne Moreau (LORIA, Nancy), Sophie Pinchinat (IRISA, Rennes), Denis Poitrenaud (LIP6, Paris), Grégoire Sutre (LaBRI, Bordeaux), Pierre Réty (LIFO, Orléans), Michaël Rusinowitch (LORIA, Nancy), Laurent Vigneron (LORIA, Nancy).
Des rencontres de deux (ou une) journée(s), en moyenne une fois par an. Elles se compléteront par des visites ``inter-équipes'' de chercheurs et de thésards, chaque fois que cela semble souhaitable sur le plan scientifique.
http://www.univ-orleans.fr/SCIENCES/LIFO/Projets/GDR/Forwal