297 lines
11 KiB
HTML
297 lines
11 KiB
HTML
<!DOCTYPE html>
|
|
<html lang="fr">
|
|
<head>
|
|
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
|
|
<link rel="stylesheet" type="text/css" href="./css/base.css?version=3">
|
|
<link rel="stylesheet" type="text/css" href="./css/man.css?version=3">
|
|
<title>Henri Saudubray</title>
|
|
<meta name="description" content="Doctorant en méthodes formelles">
|
|
<meta name="viewport" content="width=device-width, initial-scale=1.0">
|
|
</head>
|
|
<body>
|
|
<div id="pride-banner">
|
|
<div class="color yellow"></div>
|
|
<div class="color white"></div>
|
|
<div class="color purple"></div>
|
|
<div class="color black"></div>
|
|
</div>
|
|
<header>
|
|
<span>HENRI(1)</span>
|
|
<span>Informations utilisateur</span>
|
|
<span>HENRI(1)</span>
|
|
</header>
|
|
<main>
|
|
<div class="section" id="name">
|
|
<div class="section-title">Nom</div>
|
|
<div class="content">
|
|
Henri Saudubray - Doctorant en Méthodes Formelles
|
|
</div>
|
|
</div>
|
|
<div class="section" id="synopsis">
|
|
<div class="section-title">Synopsis</div>
|
|
<div class="content">
|
|
Je suis doctorant au Laboratoire Méthodes Formelles
|
|
(LMF) de l'Université Paris-Saclay. Je m'intéresse
|
|
à l'étude des langages de programmation, à la
|
|
vérification déductive, aux assistants de preuve, et à
|
|
la logique formelle.
|
|
</div>
|
|
</div>
|
|
<div class="publications" id="publications">
|
|
<div class="section-title">Publications</div>
|
|
<ul class="content">
|
|
<li>
|
|
<div class="title">
|
|
<a href="./pdf/articles/jfla-2025.pdf">
|
|
/pdf/articles/jfla-2025.pdf</a>
|
|
</div>
|
|
<div class="description">
|
|
"Faire chauffer Why3 avec de l'induction".
|
|
<br>
|
|
Décrit l'ajout d'une nouvelle construction au langage WhyML
|
|
permettant le filtrage sur les instances de prédicats
|
|
inductifs.
|
|
<br>
|
|
écrit avec
|
|
<a href="https://usr.lmf.cnrs.fr/~jcf/index.fr.html">
|
|
Jean-Christophe Filliâtre</a>
|
|
et <a href="http://www.tertium.org/">Andrei Paskevich</a>.
|
|
</div>
|
|
</li>
|
|
</ul>
|
|
</div>
|
|
<div class="section" id="teaching">
|
|
<div class="section-title">Enseignement</div>
|
|
<ul class="content">
|
|
<li>
|
|
<div class="title">
|
|
Introduction à l'informatique, L1 Informatique, UFR Sciences,
|
|
Université Paris-Saclay - Octobre 2025 - janvier 2026
|
|
</div>
|
|
<div class="description">
|
|
TD/TPs. Cours d'introduction à l'informatique : Python,
|
|
HTML/CSS, bases de réseau.
|
|
</div>
|
|
</li>
|
|
<li>
|
|
<div class="title">
|
|
Introduction à la vérification déductive, PEIP2,
|
|
Polytech Paris-Saclay - Décembre 2025 - janvier 2026
|
|
</div>
|
|
<div class="description">
|
|
Cours magistraux et TD/TPs. Cours d'introduction à la
|
|
vérification déductive avec
|
|
<a href="www.why3.org">Why3</a>.
|
|
</div>
|
|
</li>
|
|
<li>
|
|
<div class="title">
|
|
Programmation Objet et Génie Logiciel, L2 Informatique, UFR
|
|
Sciences, Université Paris-Saclay - Janvier - avril 2026
|
|
</div>
|
|
<div class="description">
|
|
TD/TPs. Génie logiciel, UML, programmation Java.
|
|
</div>
|
|
</li>
|
|
<li>
|
|
<div class="title">
|
|
Bases de données, PEIP2, Polytech Paris-Saclay - Mars - avril
|
|
2026
|
|
</div>
|
|
<div class="description">
|
|
TPs. Introduction à SQL, pandas.
|
|
</div>
|
|
</li>
|
|
</ul>
|
|
</div>
|
|
<div class="section" id="experience">
|
|
<div class="section-title">Expérience</div>
|
|
<ul class="content">
|
|
<li>
|
|
<div class="title">
|
|
<a href="https://lmf.cnrs.fr">
|
|
Laboratoire Méthodes Formelles,
|
|
Université Paris-Saclay</a>
|
|
- Depuis octobre 2025
|
|
</div>
|
|
<div class="description">
|
|
Doctorat, encadré par
|
|
<a href="https://usr.lmf.cnrs.fr/~jcf/index.fr.html">
|
|
Jean-Christophe Filliâtre</a>
|
|
et <a href="http://www.tertium.org/">Andrei Paskevich</a>.
|
|
Conception et unification des langages de programmation,
|
|
spécification et preuve dans le contexte de la
|
|
vérification déductive de programmes, au sein de l'outil
|
|
<a href="https://www.why3.org">Why3</a>.
|
|
</div>
|
|
</li>
|
|
<li>
|
|
<div class="title">
|
|
<a href="https://parkas.di.ens.fr">
|
|
INRIA, PARKAS Team</a>
|
|
- Mars - août 2025
|
|
</div>
|
|
<div class="description">
|
|
Stage de M2, encadré par
|
|
<a href="https://www.di.ens.fr/~pouzet/">Marc Pouzet</a>. Travail
|
|
autour de la reproductibilité et de la transparence des
|
|
assertions exécutables dans le langage hybride
|
|
<a href="https://zelus.di.ens.fr">Zélus</a>. Conception et
|
|
implémentation d'une
|
|
<a href="https://codeberg.org/17maiga/hsim">
|
|
sémantique exécutable</a> pour un environnement
|
|
d'exécution multi-solveur.
|
|
</div>
|
|
</li>
|
|
<li>
|
|
<div class="title">
|
|
<a href="https://lmf.cnrs.fr">
|
|
Laboratoire Méthodes Formelles, CNRS</a>
|
|
- Mars - juillet 2024
|
|
</div>
|
|
<div class="description">
|
|
Stage de M1, encadré par
|
|
<a href="https://usr.lmf.cnrs.fr/~jcf/index.fr.html">
|
|
Jean-Christophe Filliâtre</a>
|
|
et <a href="http://www.tertium.org">Andrei Paskevich</a>.
|
|
Ajout d'une nouvelle construction au langage WhyML permettant le
|
|
filtrâge sur les instances de prédicats inductifs au
|
|
sein de l'outil <a href="https://www.why3.org">Why3</a>.
|
|
Traduction d'une <a href="https://codeberg.org/17maiga/lambda">
|
|
preuve Rocq vers Why3</a> comme exemple d'utilisation.
|
|
</div>
|
|
</li>
|
|
<li>
|
|
<div class="title">
|
|
<a href="https://skapane.ai">Skapánê</a> - Septembre
|
|
2022 - août 2023
|
|
</div>
|
|
<div class="description">
|
|
Alternance en L3. Développement back-end sur une
|
|
infrastructure conteneurisée en Python et Scala. Conception
|
|
d'une plateforme de gestion d'environnements de développement
|
|
Jupyter avec React.js, Flask et Docker.
|
|
</div>
|
|
</li>
|
|
<li>
|
|
<div class="title">
|
|
<a href="https://www.icdc.caissedesdepots.fr">Informatique CDC</a>
|
|
- Mai - août 2022
|
|
</div>
|
|
<div class="description">
|
|
Stage de L2. Développement en Java d'un outil
|
|
d'automatisation de tests bout en bout et d'un convertisseur de
|
|
fichiers ISO 20022 sur l'infrastructure banquaire de la Caisse des
|
|
Dépôts et Consignations.
|
|
</div>
|
|
</li>
|
|
<li>
|
|
<div class="title">Ac'Lab - Août 2021 - mai 2022</div>
|
|
<div class="description">
|
|
Engagement associatif au sein de l'association d'informatique de
|
|
la faculté. Vice-trésorier et responsable enseignement.
|
|
Organisation d'événements, enseignement des bases du
|
|
langage Python, gestion de budget.
|
|
</div>
|
|
</li>
|
|
<li>
|
|
<div class="title">
|
|
<a href="https://www.fnacdarty.com">Fnac Darty</a> - Mai -
|
|
août 2021
|
|
</div>
|
|
<div class="description">
|
|
Stage de L1. Travail sur le parcours utilisateur sur les sites
|
|
e-commerce de Fnac et Darty. Déploiement d'une application
|
|
iOS interne.
|
|
</div>
|
|
</ul>
|
|
</div>
|
|
<div class="section" id="education">
|
|
<div class="section-title">éducation</div>
|
|
<ul class="content">
|
|
<li>
|
|
<div class="title">
|
|
<a href="https://ens-paris-saclay.fr">ENS Paris-Saclay</a> -
|
|
Septembre 2024 - mars 2025
|
|
</div>
|
|
<div class="description">
|
|
Master Parisien de Recherche en Informatique (MPRI)
|
|
</div>
|
|
</li>
|
|
<li>
|
|
<div class="title">
|
|
<a href="https://www.sciences.universite-paris-saclay.fr">
|
|
Faculté des Sciences - Université Paris-Saclay</a>
|
|
- Septembre 2023 - mars 2024
|
|
</div>
|
|
<div class="description">
|
|
Master Parisien de Recherche en Informatique (MPRI)
|
|
</div>
|
|
</li>
|
|
<li>
|
|
<div class="title">
|
|
<a href="https://www.fges.fr">FGES - Université Catholique de
|
|
Lille</a> - Septembre 2020 - mai 2023
|
|
</div>
|
|
<div class="description">
|
|
Licence Sciences du Numérique (SDN)
|
|
</div>
|
|
</li>
|
|
</ul>
|
|
</div>
|
|
<div class="section" id="files">
|
|
<div class="section-title">Fichiers</div>
|
|
<ul class="content">
|
|
<li>
|
|
<div class="title"><a href="./pdf/cv.pdf">/pdf/cv.pdf</a></div>
|
|
<div class="description">Curriculum Vitae.</div>
|
|
</li>
|
|
<li>
|
|
<div class="title">
|
|
<a href="./pdf/m1_report.pdf">/pdf/m1_report.pdf</a>
|
|
</div>
|
|
<div class="description">Rapport de stage de M1.</div>
|
|
</li>
|
|
<li>
|
|
<div class="title">
|
|
<a href="./pdf/m2_report.pdf">/pdf/m2_report.pdf</a>
|
|
</div>
|
|
<div class="description">Rapport de stage de M2.</div>
|
|
</li>
|
|
</ul>
|
|
</div>
|
|
<div class="section" id="see_also">
|
|
<div class="section-title">Liens annexes</div>
|
|
<ul class="content">
|
|
<li>
|
|
<div class="title">
|
|
<a href="mailto:hms@lmf.cnrs.fr">hms[at]lmf[dot]cnrs[dot]fr</a>
|
|
</div>
|
|
<div class="description">Email.</div>
|
|
</li>
|
|
<li>
|
|
<div class="title">
|
|
<a href="https://codeberg.org/17maiga">codeberg.org/17maiga</a>
|
|
</div>
|
|
<div class="description">Forge git.</div>
|
|
</li>
|
|
<li>
|
|
<div class="title">
|
|
<a href="https://linkedin.com/in/henri-saudubray"
|
|
>linkedin.com/in/henri-saudubray</a>
|
|
</div>
|
|
<div class="description">LinkedIn.</div>
|
|
</li>
|
|
</ul>
|
|
</div>
|
|
<div class="section" id="utils">
|
|
<a href="man.en.html">Read this page in english</a>
|
|
</div>
|
|
</main>
|
|
<footer>
|
|
<span>1.5.1</span>
|
|
<span>2025-10-20 </span>
|
|
<span>HENRI(1)</span>
|
|
</footer>
|
|
</body>
|
|
</html>
|