Je suis actuellement étudiant en M2 à l'École Normale Supérieure. Mes centres d'intérêts se situent à la frontière de l'informatique, des mathématiques et de la biologie. Ils comprennent notamment les domaines suivants : J'éprouve un plaisir tout particulier à partager ma passion pour les sciences, que ce soit dans un contexte de vulgarisation ou d'enseignement. Enfin, je suis un programmeur enthousiaste, utilisateur fanatique de langages fonctionnels fortement typés.

Stage de recherche à Harvard Medical School

J'ai effectué un stage de recherche de cinq mois à Harvard au sein du laboratoire de Walter Fontana, au cours duquel j'ai conçu un formalisme pour mieux comprendre la structure causale de certains systèmes de signalisation complexes. J'ai également développé un algorithme pour révéler cette structure dans des modèles écrits dans le langage Kappa.

Rapport de stage

Article publié à la conférence RV'15

Mon premier article scientifique, que je copublie avec Lee Pike et Alwyn Goodloe, a été accepté à la sixième conférence internationale sur la vérification à l'execution (RV'15) qui s'est tenue à Vienne en Septembre 2015. En voici le résumé (en anglais) :

Assuring the guardians

Ultra-critical systems are growing more complex, and future systems are likely to be autonomous and cannot be assured by traditional means. Runtime Verification (RV) can act as the last line of defense to protect the public safety, but only if the RV system itself is trusted. In this paper, we describe a model-checking framework for runtime mon- itors. This tool is integrated into the Copilot language and framework aimed at RV of ultra-critical hard real-time systems. In addition to de- scribing its implementation, we illustrate its application on a number of examples ranging from very simple to the Boyer-Moore majority vote algorithm.

Consulter l'article

Stage de recherche au centre NASA de Langley

J'ai passé trois mois durant l'été 2014 au NIA, centre de recherche affilié au centre NASA de Langley, sous la supervision de Mr. Alwyn Goodloe. J'ai notamment développé la bibliothèque copilot-kind, composée d'une série d'outils permettant de prouver des propriétés simples sur des programmes synchrones écrits dans le langage Copilot de manière complètement automatique. J'ai présenté une synthèse des techniques utilisées dans le cadre d'une conférence d'une heure dont je copie ci-dessous l'intitulé (en anglais) :

An insight into SMT-based model checking techniques for formal software verification

Highly automated proof techniques are a necessary step for the widespread adoption of formal methods in the software industry. Moreover, it could provide a partial answer to one of its main issue which is scalabilty. In the context of the formal verification of safety properties on synchronous dataflow programs, we examine a SMT-based approach which led to the development of the Kind2 model checker and yielded promising experimental results. We give an insight into the two algorithms powering this tool :

  • The k-induction algorithm, enriched with abstraction and path compression
  • The IC3 algorithm, with approximate quantifier elimination to generalize counterexamples

Transparents | Enregistrement vidéo

Exposé d'introduction à la théorie de la calculabilité

J'ai donné une présentation d'introduction à l'informatique fondamentale d'une heure et demie, devant la classe de HX1 du lycée Louis-Le-Grand.

Résumé

Après une introduction au formalisme des langages et des machines de Turing, on montre l'indécidabilité du problème de l'arrêt. On en mentionne deux conséquences à valeur historique que sont une version faible du théorème d'incomplétude de Gödel ainsi que la réponse négative au dixième problème de Hilbert. On étudie enfin en détail quelques propriétés des tuiles de Wang et on démontre l'indécidabilité du problème qui consiste à déterminer si un jeu de tuiles fini permet de paver le plan.

Ressources

Colles au lycée Condorcet et au lycée Louis-Le-Grand

J'ai donné des colles de mathématiques en PCSI au lycée Condorcet, puis en MPSI au lycée Louis-Le-Grand, à raison de 2h par semaine. Quelques exemples de fiches d'exercices donnés au élèves sont recensés ci-dessous.

  • Feuille 1 : nombres complexes, trigonométrie
  • Feuille 2 : nombres complexes, équations différentielles
  • Feuille 3 : équations différentielles, ensembles
  • Feuille 4 : ensembles, dénombrement
  • Feuille 5 : calculs algébriques, ensembles, dénombrement
  • Feuille 6 : suites et limites

Sur la complexité du Sokoban

J'ai travaillé sur la complexité du jeu de Sokoban dans le cadre de l'épreuve de TIPE du concours des ENS. Dans des termes techniques, j'ai présenté une preuve originale de la PSPACE-difficulté du sokoban par réduction polynomiale au problème QSAT. Ce résultat signifie en particulier que si un algorithme efficace répondant à la question "Ce niveau de Sokoban admet-t-il une solution ?" est trouvé, alors nous serions en mesure d'en déduire une série d'algorithmes pour résoudre toute une classe de problèmes ouverts dits NP-complets, incluant par exemple le célèbre problème du voyageur de commerce. On répondrait enfin de manière positive à la question "P=NP ?", qui constitue sans doute une des plus belles énigmes de l'informatique fondamentale.

Ce travail a obtenu la note maximale à l'épreuve de TIPE des ENS, et a été présenté dans le cadre du 54ème Séminaire des élèves du lycée Louis Le Grand.

Article contenant la démonstration | Transparents utilisés lors de l'épreuve de TIPE



Thème inspiré de : Hemingway.

Pages d'amis