Les intervenant•e•s d'Horizon Maths 2024

Sylvie Boldo est chercheuse en informatique. Ses recherches concernent à la fois la formalisation des mathématiques et l'arithmétique des ordinateurs, notamment la vérification formelle des programmes et algorithmes utilisant l'arithmétique à virgule flottante. Elle est directrice de recherche à Inria, affiliée au laboratoire de méthodes formelles de l'université Paris-Saclay et au centre de recherche Inria Saclay-Île-de-France. Elle est également la première présidente du jury de l'agrégation française d'informatique.
En savoir plus : https://pages.saclay.inria.fr/sylvie.boldo/

Catherine Dubois est professeure à l'ENSIIE et membre de l'équipe Méthodes du laboratoire Samovar depuis le 1er janvier 2016. Elle est actuellement en délégation dans l'équipe-projet Deducteam de INRIA Saclay au laboratoire LMF. Elle est co-directrice du GDR GPL (Génie de la programmation et du Logiciel) depuis le 1^er janvier 2021. Elle a précédemment été responsable de l'équipe Conception et Programmation Raisonnées (CPR) du laboratoire Cedric jusqu'en juillet 2015 et co-responsable du groupe de travail LTP (Langages, Types et Preuves) du GDR GPL jusqu'en avril 2015. Ses principaux thèmes de recherche actuels sont la sémantique des langages de programmation, la preuve formelle et l'interopérabilité des outils de preuve. 
En savoir plus : http://web4.ensiie.fr/~dubois/

Danko Ilik est spécialiste du logiciel au sein du Service de sûreté de fonctionnement de la Direction du transport spatial du CNES. Après une carrière d’enseignant-chercheur en logique et en langages de programmation, il a travaillé pendant quelques années sur l’application de la preuve mathématique dans les domaines des trains autonomes et de la cyber-sécurité. Actuellement, il s’intéresse à la sûreté de fonctionnement plus largement et en particulier à la prise en compte des pannes aléatoires dans la méthodologie de développement et de validation des systèmes critiques.
En savoir plus : https://iaddg.net/danko/CV.html

Jacques-Henri Jourdan est chargé de recherche CNRS au LMF (Laboratoire Méthodes Formelles), Université Paris- Saclay, ENS Paris-Saclay, depuis 2017. Diplômé de l'ENS Paris, il a auparavant effectué un postdoctorat au Max Plank Institute for Software Systems sur le projet RustBelt : étude et preuve formelle en Coq du système de types du langage Rust à l’aide de la logique de séparation concurrente Iris. Sa thèse, effectuée dans l’équipe Inria Gallium et soutenue à l'Université Paris-Diderot (aujourd'hui Université Paris Cité), avait obtenu le prix de thèse 2016 du GdR GPL. Il est également lauréat du prix Alonzo Church pour la conception et la mise en oeuvre de la plateforme Iris.
En savoir plus : https://jhjourdan.mketjh.fr

Thierry Lecomte est directeur R&D de CLEARSY, une PME française spécialisée dans l'invention de systèmes sûrs critiques, où il travaille depuis 2001 pour des projets industriels dans les domaines de la mobilité automatique et autonome terrestre et marine, de la santé, de la microélectronique, de l'énergie nucléaire et de l'espace.  Ses sujets d'intérêt actuels sont la co-ingénierie de la sûreté et de la sécurité, l'intelligence artificielle sûre et la mobilité autonome, tous liés aux méthodes formelles.
En savoir plus : https://www.linkedin.com/in/thierry-lecomte-19695b

Xavier Leroy est professeur du Collège de France, titulaire de la chaire Sciences du logiciel, et membre de l'Académie des sciences.  Ses travaux portent sur les langages et outils de programmation et sur la vérification formelle de logiciels critiques.  Il est auteur de deux grands logiciels issus de la recherche, le langage de programmation fonctionnelle OCaml et le compilateur formellement vérifié CompCert.
En savoir plus : https://www.college-de-france.fr/fr/chaire/xavier-leroy-sciences-du-logiciel-statutory-chair/biography

Gregory Malecha est directeur des méthodes formelles chez BedRock Systems, où il dirige une équipe d'ingénieurs dans le développement et l'application d'outils pour prouver des propriétés profondes sur le code de bas niveau. Il a obtenu son doctorat à Harvard en 2014 sur les techniques évolutives de vérification dans les assistants de preuve fondamentaux. Avant BedRock, il a appliqué ces techniques à des systèmes cyber-physiques, des applications web et une base de données relationnelle.
En savoir plus : https://gmalecha.github.io

Après une formation en informatique théorique à l'ÉNS Lyon puis une thèse en 2013, Pierre Roux est aujourd'hui chargé de recherche à l'ONERA. Il y poursuit des travaux sur l'application des méthodes formelles aux systèmes embarqués aéronautiques, avec un intérêt particulier pour les assistants de preuve, l'optimisation convexe et l'arithmétique à virgule flottante.
En savoir plus : https://www.onera.fr/fr/staff/pierre-roux

Pierre-Yves Strub est chercheur à PQShield. Ses recherches se focalisent sur la conception et l'implémentation d'outils formels d'aide à la construction et la vérification de preuves de sécurité. Ses axes de recherche sont à la croisée de plusieurs domaines: langage de programmation, cryptographie, preuve formelle, formalisation des mathématiques.
Pierre-Yves Strub est un des auteurs principaux de EasyCrypt, un assistant à la preuve dédié à la formalisation de propriétés de sécurité, dans le modèle calculatoire, de primitives cryptographiques.
En savoir plus : http://www.strub.nu

Laurent Voisin applique depuis plus de 20 ans des méthodes formelles dans l'industrie, essentiellement dans le domaine ferroviaire.  Il est également l'architecte principal de Rodin, la plate-forme de référence pour la modélisation formelle de systèmes en B événementiel.
En savoir plus : https://blog.systerel.fr/fr/authors/laurent-voisin/

Retour au programme de la conférence.