Villeurbanne Cedex
Après un post-doctorat en tant qu'ingénieur expert à l'INRIA-Saclay Ile de France, je suis maintenant maître de conférence à l'INSA de Lyon depuis le 1er septembre 2008.
Durant mon post-doctorat j'ai travaillé à la définition d'un langage de haut niveau d'expression de propriétés de sécurité pouvant se réécrire sous la forme d'annotations Pré/Post et permettant d'exprimer de bonnes propriétés de confidentialité et d'intégrité sur des systèmes de bas niveau développés en C (incluant des routines assembleur et des accès en mémoire partagée).
Mes résultats on porté sur une extension de la logique LTL et les travaux initiaux de Julien Groslambert. L'approche consiste alors à réécrire la formule LTL sous la forme d'un automate de Büchi, lequel est ensuite réécrit sous la forme d'annotations en logique du premier ordre.
J'ai également été invité par Jean-François Couchot à réfléchir avec lui à des problèmes d'automatisation de la résolution d'obligations de preuve. Ma participation a principalement porté sur l'apport d'un jeu de tests, la recherche manuelle d'heuristiques automatisables et la mise à jour de son outil.
Mes travaux actuels sont la continuité de mes travaux passés, mais dans lesquels j'essaie d'ajouter une coloration réseaux de capteurs/système embarqués afin de me rapprocher des thématiques de recherche de ma nouvelle équipe d'accueil.
Mes compétences :
Methode B
Sécurité
Validation
