TOULOUSE
Docteur de l'université de Toulouse, je suis actuellement employé au CEA/ List, laboratoire de Sécurité du Logiciel, J’y travaille sur la vérification formelle de programmes quantiques. Plus précisément , je développe un langage noyau appelé proto-quaml, qui permet l’écriture de programmes de construction de circuits quantiques, Proto-quaml est embarqué dans le langage WhyMl, un langage type ML conçu pour la vérification formelle de programmes fonctionnels annotés, Grace à l’outil de vérification et de « preuve interactive » Why3, un programme WhyML génère des obligations de preuves formatées pour différents SMT solver ou assistants de preuves,
Ceci permet donc l’écriture d’un langage quantique entièrement certifié et d’outils de vérification de correction pour les programmes écrits dans ce langage, Je développe en ce moment le noyau du langage ainsi que sa sémantique matricielle. Je projette à court terme de l’illustrer via l’écriture d’un programme entièrement certifié d’implémentation de l’algorithme de Shor,
Auparavant, j’ai effectué ma thèse à L’Onera à Toulouse, J’y développé un langage de modélisation pour l'ingénierie des exigences (khi) . J'ai également introduit la notion de raffinement de stratégies pour des agents dans les logiques temporelles multi-agents (Logique USL). Ceci permet en particulier de vérifier la capacité d'agents en interactions à satisfaire les différentes exigences qui leurs sont assignées dans Khi. Ces travaux ont trouvé un prolongement au LORIA, à Nancy, (septembre 2016 – décembre 2017) sur les jeux à information imparfaite. J’y ai développe un langage formel, PKSL, qui permet de discuter des capacités qu'ont des agents de satisfaire des buts, dans un contexte d'interaction, selon la connaissance qu'ils ont de ce contexte et de son évolution passée. Cette approche est illustrée notamment en sécurité, pour caractériser la détection d'une intrusion par un agent malveillant dans un système.
En postdoc à l'école Polytechnique de Montréal durant l'année 2015, j'ai également travaillé, au sein d'un projet industriel, sur le model-checking appliqué aux systèmes avioniques : j'ai développé un langage de modélisation pour les architectures IMA interconnectés par des réseaux TTEthernet, formalisé cette modélisation dans le langage d'entrée de NuSMV et développé en java des méthodes d'écritures pour ce code NuSMV et de transformation/abstraction des modèles.
Page personnelle : sites.google.com/site/christophechareton/
Mes compétences :
Model-checking
Méthodes formelles
NuSMV
Java
Latex
Ingénierie des exigences
Modélisation-UML
