Actualités > Seminaire de Adrien Champion
Retenez la date !
Le prochain séminaire de recherche du L3i aura lieu le jeudi 26 avril à 14h en salle 018 du bâtiment Pascal (Faculté des Sciences et Technologies, av. Henri Becquerel, 17000 La Rochelle).
Nous recevons Adrien Champion, chercheur à l’Université de Tokyo dans l’équipe de Naoki Kobayashi et travaillant sur la vérification de programmes fonctionnels d’ordre supérieur. Il viendra nous présenter ses travaux et discuter avec les membres du laboratoire intéressés par ses thématiques de recherche autour des méthodes formelles. Un temps d’échanges sera prévu à l’issue du séminaire.
Titre :
Formal Methods : Building Blocks, (Critical) Embedded System Model-Checking and (Generic) Software Verification
Résumé du séminaire :
Ce séminaire présentera les outils et techniques de vérification actuelles. Il s’inscrit plus généralement dans la thématique des "méthodes formelles" dans la mesure où ces outils et techniques peuvent également servir, par exemple, à générer des tests automatiquement à partir d’une spécification.
Aucune expertise dans le domaine n’est nécessaire, bien que quelques connaissances en logique du premier ordre et en systèmes de transitions permettraient de saisir plus aisément certains points techniques.
Découpé en trois parties, le séminaire commencera par introduire la brique de base de l’extrême majorité des techniques de vérification actuelles : les solveurs SMT (Satisfiability Modulo Theory).
La deuxième partie sera consacrée à la vérification de systèmes embarqués critiques. Présents dans l’industrie du transport (automobile, aéronautique, spatial...), mais aussi dans le médical, ces systèmes ont des structures particulières, différentes des programmes issus du logiciel, typiquement représentées par des systèmes de transitions. A haut niveau d’abstraction, les techniques de vérification de ce domaine sont relativement simples à comprendre car toutes sont explicitement basées sur la notion d’induction.
Le séminaire terminera par une discussion sur la vérification de programmes génériques. La façon de représenter ces programmes et de penser leur vérification contraste avec l’embarqué critique, et ressemble davantage à un problème de synthèse de "contrats" ou "types" pour les différents composant du programme Malgré cela, les techniques de vérification logicielle sont étonnemment proches de celles de l’embarqué critique, au moins sur le plan théorique.
Biographie de l’invité :
Adrien Champion est chercheur à l’Université de Tokyo dans l’équipe de Naoki
Kobayashi et travaille sur la vérification de programmes fonctionnels d’ordre supérieur. Sa spécialité est la mise au point et l’implementation de techniques de vérification, en s’appuyant sur les solveurs SMT, l’induction, le machine learning...
Rochelais d’origine, il a fait ses études à l’ENSEEIHT de Toulouse avant d’obtenir son doctorat de l’INP Toulouse à l’ONERA, en thèse CIFRE avec Rockwell-Collins France. Son domaine était à l’époque la verification de systèmes embarqués critiques, en particulier dans l’avionique.
Il est ensuite parti pour l’Iowa dans l’équipe de Cesare Tinelli afin de travailler sur le model-checker Kind 2 dans le cadre d’un projet avec la NASA.
Le projet portait sur la vérification compositionnelle, afin de permettre a Kind 2 de vérifier une partie relativement importante d’un système auto-pilote d’avion de ligne.
https://www.researchgate.net/profile/Adrien_Champion
https://github.com/AdrienChampion
https://www.linkedin.com/in/adrienchampion