Fondement des automates à pile – LIFOUNDATIONS

Les modèles à pile fournissent un cadre mathématique pour modéliser le comportement des programmes séquentiels. Ce sont essentiellement des automates finis qui peuvent utiliser une mémoire de type "premier entré" / "dernier sorti". Les automates à pile sont probablement le modèle le plus connu de ce type. Ils permettent de modéliser fidèlement les programmes récursifs utilisant des variables booléennes.

Ce projet contribue à améliorer notre compréhension des modèles à pile, des modèles centraux dans la vérification automatique de programmes séquentiels. Le projet étudie trois questions majeures dans ce contexte : le problème de la sous-classe (qui consiste à décider si un programme est équivalent à un programme d'une sous-classe sémantique ou syntaxique), le problème de la complexité (qui consiste à décider si le calcul d'un programme peut être réalisé en utilisant des ressources limitées) et enfin le problème de l'équivalence (qui consiste à décider si deux programmes sont équivalents).

Bien que durant les 25 dernières années de nombreux résultats de décidabilité ont été établis, de nombreuses questions restent ouvertes et échappent parfois à notre compréhension.

Le but de ce projet est d'améliorer notre compréhension des modèles à pile suivant trois axes: les problèmes de sous-classes, la compréhension de leur complexité algorithmique et les problèmes d’équivalence.