Section: Dissemination

Teaching - Supervision - Juries

Teaching

• Master Parisien de Recherche en Informatique (MPRI) https://wikimpri.dptinfo.ens-cachan.fr/doku.php: “Proofs of Programs” http://www.lri.fr/~marche/MPRI-2-36-1/ (M2), C. Marché (12h).

• A. Lanco, Unix et programmation Web, 24h, L2, Université Paris-Saclay, France.

• G. Melquiond, Programmation C++ avancée, 12h, M2, Université Paris-Saclay, France.

• J.-C. Filliâtre, Langages de programmation et compilation, 25h, L3, École Normale Supérieure, France.

• J.-C. Filliâtre, Les bases de l'algorithmique et de la programmation, 15h, L3, École Polytechnique, France.

• J.-C. Filliâtre, Compilation, 18h, M1, École Polytechnique, France.

• S. Boldo was invited in the Xavier Leroy's course at Collège de France on Dec 19th.

Supervision

• HDR: G. Melquiond, “Formal Verification for Numerical Computations, and the Other Way Around” [11], Université Paris-Sud, Apr. 1st, 2019.

• PhD: F. Faissole, “Formalisations d'analyses d'erreurs en analyse numérique et en arithmétique à virgule flottante”, Université Paris-Saclay & Université Paris-Sud, Dec 13th 2019, supervised by S. Boldo and A. Chapoutot. [Not yet on HAL]

• PhD: A. Coquereau, “Amélioration de performances du solveur SMT Alt-Ergo grâce à l’intégration d’un solveur SAT efficace”, Université Paris-Saclay & Université Paris-Sud, Dec 16th 2019, supervised by S. Conchon, F. Le Fessant et M. Mauny. [Not yet on HAL]

• PhD: M. Roux, “Extensions de l’algorithme d’atteignabilité arrière dans le cadre de la vérification de modèles modulo théories”, Université Paris-Saclay & Université Paris-Sud, Dec 19th 2019, supervised by Sylvain Conchon. [Not yet on HAL]

• PhD in progress: R. Rieu-Helft, “Développement et vérification de bibliothèques d'arithmétique entière en précision arbitraire”, since Oct. 2017, supervised by G. Melquiond and P. Cuoq (TrustInSoft).

• PhD in progress: D. Gallois-Wong, “Vérification formelle et filtres numériques”, since Oct. 2017, supervised by S. Boldo and T. Hilaire.

• PhD in progress: Q. Garchery, “Certification de la génération et de la transformation d’obligations de preuve”, since Oct. 2018, supervised by C. Keller, C. Marché and A. Paskevich.

• PhD in progress: A. Lanco, “Stratégies pour la réduction forte”, since Oct. 2019, supervised by T. Balabonski and G. Melquiond.

• G. Turbiau has been a M1 trainee for 2 months, supervised by S. Boldo.

Juries

• S. Boldo, member of the Inria CRCN recruiting juries, national one and at Rennes.

• S. Boldo, president of the PhD defense of Clothilde Jeangoudoux, Sorbonne University, May 21st

• S. Boldo, reviewer of the habilitation of Christoph Lauter, Sorbonne University, May 22nd

• S. Boldo, reviewer of the PhD defence of Florent Bréhard, ENS Lyon, July 12th

• S. Boldo, reviewer of PhD defence of Damien Rouhling, Université Côte d'Azur, Sept 30th

• S. Boldo, president of the PhD defense of Yohan Chatelain, Université Paris-Saclay, Dec 12th

• S. Boldo, president of the PhD defense of Armaël Guéneau, Université de Paris, Dec 16th

• S. Boldo, member of the PhD defense of Antoine Kaszczyc, Université Paris-Nord, Dec 18th

• J.-C. Filliâtre, reviewer of the PhD defense of Y. El Bakouny, “Scallina: On the Intersection of Scala and Gallina”, Université Saint-Joseph, Beirut, Lebanon, December 19, 2019.

• J.-C. Filliâtre, president of the PhD defense of L. Blatter “Relational properties for specification and verification of C programs in Frama-C”, University Paris Saclay, September 26, 2019.