Sylvain SCHMITZ

Statut

Maître de conférences

Promotion

Junior 2018

Établissement

Université de Paris

Secteur disciplinaire

Sciences et Technologies de l'Information et de la Communication

Spécialité

Discipline Informatique - Logique et vérification

Thématique

► Vérification
► Logique informatique
► Méthodes formelles
► Langages formels
► Complexité algorithmique

Présentation

Les techniques de raisonnement automatique pour les programmes, algorithmes distribués, systèmes embarqués, …, cherchent des procédures de décisions qui trouvent un bon compromis entre expressivité et complexité algorithmique. Le projet se concentre sur deux familles de modèles centrés sur les ressources.

La première famille contient des extensions des systèmes d’addition de vecteurs. Le principal problème ouvert dans ce domaine est le problème d’accessibilité. Répondre à ce problème pour ces extensions aurait un impact majeur pour de nombreux problèmes liés en logique, vérification, XML, calcul distribué, linguistique informatique, cryptographie, … Une approche prometteuse est d’employer des techniques de décomposition en idéaux de beaux pré-ordres, qui fournissent un cadre abstrait pour l’accessibilité dans les systèmes d’addition de vecteurs. Je propose d’étendre et d’affiner ces techniques, et d’étudier les propriétés, les représentations finies, et l’algorithmique des idéaux.

La seconde famille est celle des systèmes dynamiques centrés sur les données, qui modélisent les interactions entre une base de données et des processus logiques. Dans ce cadre, je compte étudier des variantes d’une conjecture due à Lasota sur le lien entre la décidabilité de la sûreté de tels systèmes et l’existence d’un beau pré-ordre sur la base de données.

Anciennement Maître de conférences à l'École Normale Supérieure.

Revenir