Laboratoire	LIX, UMR 4073
Nom de l'équipe ou du projet	Récriture et Preuve
Responsable	Jean-Pierre Jouannaud (jusqu'en septembre)
Effectifs (chercheurs, enseignants-chercheurs, thésards, ingénieurs, techniciens)	2 PR, 1 MDC, 1 postdoc a la rentreL'équipe recevra le renfort de la partie INRIA-futurs du projet LOGICAL au cours du premier semestre de l'année 2003.
Axes de recherche (liste de mots-clefs)	Preuve formelle Preuves modulo Automatisation des systèmes de preuves par utilisation de récriture Spécification de systèmes temps réel en logique linéaire Logique linéaire et automates Preuves contraintes en ressources.
Relations industrielles ( liste de partenaires industriels)	France Telecom
Participation à des programmes nationaux (ex. RNTL, RNRT) (liste de projets)	RNRT: Calife RNTL: Averroes
Participation à des programmes européens (ex. IST) (liste de projets)	aucun au titre du LIX
Plates-formes	Coq et ses prototypes de développement au titre deLOGICAL
Suggestions	Nous sommes très intéressés par les questions de sécurité de protocoles cryptographiques, a cause de l'existence dans le laboratoire de l'action INRIA-Futurs TANC (Théorie Algorithmique des Nombres pour la Cryptographie), et des applications que développe cetteéquipe en liaison avec GEMPLUS. Une Action Spécifique sur la "sécurité" qui intégrerait des aspects Cryptographie, Vérification de protocoles cryptographique, et Détection d'intrusions me semblerait une bonne idée. Identifier les problématiques et verrous sur ces questions pourrait un jour donner lieu a un projet national ou même européen d'envergure, mesemble-t-il.