Équipe : SPI - Sémantique Preuves Implantation

L'équipe SPI (Sémantique, Preuves et Implantation) travaille sur la conception et la réalisation de l'atelier Focal. Cet atelier permet de décrire la spécification d'un système par des propriétés puis de passer progressivement à l'implantation de ce système, tout en démontrant que les propriétés attendues sont bien vérifiées. Des outils puissants (héritage multiple, liaison retardée, redéfinition, paramétrisation générique de haut niveau) sont proposés dans cet atelier. Un source Focal est formé de déclarations, définitions, propriétés et preuves est compilé vers un source Ocaml exécutable, vers un chapitre Coq vérifiable par Coq et ves un langage de documentation, qui permet la création de fichiers de documentation sous différents formats. Les preuves peuvent être faites à l'aide d'un outil de démonstration automatique, Zenon, qui, s'il réussit la preuve, en donne une trace sous forme d'un terme Coq. Si Zenon échoue, la preuve peut être faite directement dans Coq. La distribution de Focal vient avec une importante biliothèque de calcul formel. Focal est également utilisé pour modéliser des propriétés de sécurité. En effet, l'équipe travaille également à la construction de modéles formels de sécurité permettant de comparer par exemple des modes d'accès différents. L'équipe est également impliquée dans le développement d'outils de démonstration automatique fondés sur le calcul des Séquents Modulo.
Les travaux sont menés en collaboaration très étroite avec l'équipe CPR du Laboratoire CEDRIC du CNAM et des chercheurs de l'INRIA.