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. Charguéraud (12h), Université Paris-Diderot, France.

• Master: Fondements de l'informatique et ingénierie du logiciel (FIIL) https://www.lri.fr/~conchon/parcours_fiil/: “Software Model Checking” (M2), S. Conchon (9h), “Programmation C++11 avancée” (M2), G. Melquiond (12h), “Vérification déductive de programmes” (M2), A. Paskevich (10.5h), Université Paris-Sud, France.

• DUT (Diplôme Universitaire de Technologie): M1101 “Introduction aux systèmes informatiques”, A. Paskevich (36h), M3101 “Principes des systèmes d'exploitation”, A. Paskevich (58.5h), IUT d'Orsay, Université Paris-Sud, France.

• Licence: “Langages de programmation et compilation” (L3), J.-C. Filliâtre (26h), École Normale Supérieure, France.

• Licence: “INF411: Les bases de l'algorithmique et de la programmation” (L3), J.-C. Filliâtre (16h), École Polytechnique, France.

• Licence: “Programmation fonctionnelle avancée” (L3), S. Conchon (45h), Université Paris-Sud, France.

• Licence: “Introduction à la programmation fonctionnelle” (L2), S. Conchon (25h), Université Paris-Sud, France.

Internships

• Raphaël Rieu-Helft (ENS, Paris) is a pre-PhD student doing an internship for 6 months under supervision of C. Marché, G. Melquiond and A. Paskevich. He is working on the design and the formal verification of a library for unbounded integer arithmetic. Why3 is used for formally verifying the functional behaviour of the library operations. Raphaël is also implementing in Why3 a mechanism for extracting code to the C language, in order to obtain a certified code that runs very efficiently.

• Lucas Baudin (ENS, Paris) is a master 1 intern under the supervision of J.-C. Filliâtre between September 2016 and January 2017. He is working on the inference of loop invariants by abstract interpretation in the tool Why3.

• F. Faissole was a master 2 trainee under the supervision of S. Boldo between March and August 2016. He worked on the formal proof of the Lax-Milgram theorem.

Supervision

• PhD: L. Gondelmans, “Obtention de programmes corrects par raffinement dans un langage de haut niveau”, Université Paris-Saclay & Université Paris-Sud, December 13, 2016, supervised by J.-C. Filliâtre and A. Paskevich.

• PhD in progress: M. Clochard, “A unique language for developing programs and prove them at the same time”, since Oct. 2013, supervised by C. Marché and A. Paskevich.

• PhD in progress: D. Declerck, “Vérification par des techniques de test et model checking de programmes C11”, since Sep. 2014, supervised by F. Zaïdi (LRI) and S. Conchon.

• PhD in progress: M. Roux, “Model Checking de systèmes paramétrés et temporisés”, since Sep. 2015, supervised by Sylvain Conchon.

• PhD in progress: M. Pereira, “A Verified Graph Library. Tools and techniques for the verification of modular higher-order programs, with extraction”, since May 2015, supervised by J.-C. Filliâtre.

• PhD in progress: A. Coquereau, “[ErgoFast] Amélioration de performances pour le solveur SMT Alt-Ergo : conception d'outils d'analyse, optimisations et structures de données efficaces pour OCaml”, since Sep. 2015, supervised by Sylvain Conchon, Fabrice Le Fessant et Michel Mauny.

• PhD in progress: F. Faissole, “Stabilité(s): liens entre l'arithmétique flottante et l'analyse numérique”, since Oct 2016, supervised by S. Boldo and A. Chapoutot.

Juries

• J.-C. Filliâtre: president of the PhD committee of A. Djoudi, “Analyse statique au niveau binaire”, Université Paris Saclay, France, December 2016.

• S. Conchon: examiner of the PhD of M. Morterol,“Méthodes avancées de raisonnement en logique propositionnelle : application aux réseaux métaboliques”, Université Paris-Saclay, December 2016.

• S. Conchon: reviewer of the PhD of A. Blanchard, “Aide à la vérification de programmes concurrents par transformation de code et de spécifications”, Université d'Orléans, December 2016.

• S. Conchon: reviewer of the HDR of X. Thirioux, “Verifying Embedded Systems”, Institut National Polytechnique de Toulouse, September 2016.

• S. Conchon : examiner of the PhD of L. Cabaret, “Algorithmes d'étiquetage en composantes connexes efficaces pour architectures hautes performances”, September 2016.