Vérification Formelle des Automates et Réalisabilité Optimisée – FAVOR

Implémenter manuellement un programme complexe est une tâche difficile, et il est compliqué d’éviter les erreurs, ce qui est inacceptable pour les applications critiques où la précision est primordiale.
La vérification formelle cherche à développer des méthodes qui garantissent la correction des programmes,
ou qui génèrent automatiquement des programmes corrects à partir de spécifications définissant le comportement souhaité.
Ces méthodes permettent de produire des outils puissants qui peuvent libérer les utilisateur·rice·s de la nécessité de programmer manuellement.
Cependant, leurs applications pratiques sont souvent limitées par des contraintes théoriques :
pour des systèmes complexes et réalistes, ces problèmes sont souvent indécidables ou entraînent des coûts de calcul prohibitifs.
L'objectif du projet FAVOR est de surmonter ces limitations en renforçant les fondations théoriques de la vérification formelle.
Le projet vise à étendre la gamme des machines abstraites pouvant être vérifiées et synthétisées, et à identifier les sources de la complexité algorithmique élevée.