Le séminaire Vérification et Preuves

Le séminaire SVP a lieu tous les deux mois, en alternance entre le LRI et le LSV. Le séminaire est public et ne nécessite aucune inscription préalable.

Séminaires passés

Les données font leurs preuves

Véronique Benzaken
Date
Le vendredi 31 mars 2017 à 11:00
Lieu
LRI (grand amphi du PUIO bat 640)
Orateur
Véronique Benzaken (LRI)

Les données sont omniprésentes et précieuses. De façon surprenante peu d'attention a été consacrée pour garantir, de manière indiscutable, que les sytèmes en charge de leurs traitements sont sûrs. Une approche prometteuse afin d'obtenir des garanties fortes est d'utiliser des assistants à la preuve tels Coq. Dans cet exposé nous nous intéresserons aux systèmes relationnels qui sont parmi les plus répandus et tout particulièrement à la chaine de compilation de SQL. Nous décrirons les différentes étapes indispensables à l'obtention d'une chaine de compilation certifiée : spécification extrême, en Coq, du modèle relationnel, mécanisation, en Coq, de la sémantique de SQL, analyse syntaxique et sémantique certifiée et optimisation vérifiée.

À propos du LSV