Room 206 (2nd floor, badged access)
23 novembre 2021 - 14h00
Conception, développement et certification dans Coq/MathComp d'optimisations Datalog pour la vérification réseau (Phd Defense)
par PIERRE-LEO BEGAY de Orange Labs & Verimag
Résumé : Nous introduisons une analyse statique et deux transformations de programmes pour Datalog dans le but de résoudre des problèmes de performance liés à l'implémentation de certaines primitives, notamment dans le cadre de la vérification d'applications de télécommunications à grande échelle. L'analyse et les réécritures sont certifiées à l'aide de DatalogCert, une formalisation Coq/MathComp de Datalog préexistante. Pour ce faire, nous introduisons une nouvelle sémantique de trace pour Datalog avec un opérateur vérifié. Ce travail pour être vu à la fois comme une première étape et un proof of concept pour la création d'une bibliothèque complète d'optimisations Datalog vérifiées à l'aide de DatalogCert, dans l'objectif final de développer un environnement réaliste pour des applications orientées données certifiées.
