Publication


Rapports

Vérification par preuve formelle de propriétés fonctionnelles d'algorithmes de classification

Ce document est un rapport de mes travaux en tant qu'ingénieur d'étude sur le sujet Vérification par preuve formelle de propriétés fonctionnelles d'algorithmes de classification, effectués dans le cadre de ma formation en Magistère 2 d'Informatique à l'Université Paris-Sud. J'y présente la preuve formelle par vérification déductive de propriétés des algorithmes de Parcoursup' au moyen de Why3. J'ai été encadré par Jean-Christophe Filliâtre.

Un pdf est disponible: internship-report-parcoursup.pdf. Le code source aussi: internship-report-parcoursup.

Partage d'implémentation, implémentation du partage: une bibliothèque fonctorisée de diagrammes de décision binaires

Ce document est un rapport de mes travaux de recherche sur le sujet Partage d'implémentation, implémentation du partage: une bibliothèque fonctorisée de diagrammes de décision binaires, effectués dans le cadre de ma formation en Master 1 Informatique à l'Université Paris-Saclay, j'ai été encadré par Jean-Christophe Filliâtre.

Un pdf est disponible: ter-report.pdf. Le code source aussi: ter-report.

Le psittacisme pour permettre l'oubli motivé : implémentation et vérification du lambda lifting pour le compilateur CakeML

Ce document est un rapport de mon stage Le psittacisme pour permettre l'oubli motivé : implémentation et vérification du lambda-lifting dans le compilateur CakeML, effectué dans le cadre de ma formation en Master 1 Jacques Herbrand à l'École Normale Supérieure Paris-Saclay. Ce stage s'est déroulé sous la direction conjointe de Scott Owens et de Hugo Férée.

Un pdf est disponible: internship-report-cakeml.pdf. Le code source aussi: internship-report-cakeml.

Vérification de compilation de requêtes SQL à base de traces

Ce document est un rapport de mon stage Vérification de compilation de requêtes SQL à base de traces, effectué dans le cadre de ma formation en Magistère 1 à l'Université Paris-Sud. Ce stage s'est déroulé sous la direction conjointe de Véronique Benzaken, Évelyne Contejean et Chantal Keller.

Un pdf est disponible: internship-report-datacert.pdf. Le code source aussi: internship-report-datacert.

Posters

Deep specification and verification of SQL compilation chain

Ce document est un poster que j'ai réalisé et qui a été présenté par Raphaël Cornet à la Junior Conference on Data Science and Engineering 2017. Il porte sur le travail effectué au cours de mon stage Vérification de compilation de requêtes SQL à base de traces, ainsi que sur les stages de Raphaël Cornet et d'Eunice Martins.

Un pdf est disponible: poster-jdse-2017.pdf. Le code source aussi: poster-jdse-2017.