EN FR
EN FR


previous Previous | up Home | Next next


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/ : “Programmation C++11 avancée” (M2), G. Melquiond (18h), “Preuves Interactives et Applications” (M2), C. Paulin (9h), “Vérification déductive de programmes” (M2), A. Paskevich (11.5h), Université Paris-Sud, France.

  • Licence: “Mathématiques pour l'informatique 2” (L2), C. Paulin (50h), Université Paris-Sud, France.

  • Licence: “Logique pour l'informatique” (L3), C. Paulin (54h), Université Paris-Sud, France.

  • Master: “Logique pour l'option informatique à l'agrégation” (M2), C. Paulin (21h), ENS Cachan, France.

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

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

  • Master: “Compilation et langages” (M1), S. Conchon (45h), Université Paris-Sud, France.

  • Master: “Software Model Checking” (M2), S. Conchon (10h), 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.

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

Internships

  • S. Conchon supervised the M2 internship of Mattias Roux, who developed a new reachability algorithm for the Cubicle Model Checker.

  • A. Charguéraud supervised, with F. Pottier (Inria Paris) the M2 internship of Armaël Guéneau, who developed a formalization in Coq of the big-O notation, and put it to practice to establish big-O asymptotic bounds in CFML, in particular for a sequence data structure with logarithmic-time random access operations.

  • C. Paulin supervised with F. Hivert (LRI) the magistère of Mathematics internship of Olivier Stietel, who developed a proof in Coq of a result in combinatorics (a result of Frame, Robinson and Thrall counting the number of Young tableaux of a given shape) using a probabilistic method.

Supervision

  • PhD: C. Lelay, “Repenser la bibliothèque réelle de Coq : vers une formalisation de l'analyse classique mieux adaptée”, Université Paris-Sud, June 15th 2015, supervised by S. Boldo and G. Melquiond [11] .

  • PhD in progress: S. Dumbrava, “Towards data certification”, since Oct. 2012, supervised by V. Benzaken (LRI) and É. Contejean.

  • PhD in progress: L. Gondelmans, “Obtention de programmes corrects par raffinement dans un langage de haut niveau”, since Oct. 2013, 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.

Juries

  • S. Boldo: reviewer, PhD committee of O. Kupriianova, “Towards a Modern Floating-Point Environment”, Université Pierre et Marie Curie, France, December 2015.

  • A. Charguéraud: examiner, PhD committee of Lidia Sánchez Gil, “On the equivalence of operational and denotational semantics for parallel functional languages”, Universidad Complutense de Madrid, July 2015.

  • C. Marché: reviewer, PhD committee of A. Dieumegard, “Formal Guarantees for Safety Critical Code Generation: The Case of Highly Variable Languages”, Université Toulouse 3 Paul Sabatier, France, January 2015.

  • C. Marché: external reviewer of the PhD memoir of D. Larraz, “Automatic Program Analysis using Max-SMT”, Universitat Politecnica de Catalunya, Barcelona, Spain, April 2015.

  • C. Marché: president of the PhD committee of A. David, “Vers la synthèse de systèmes ouverts : tableaux pour les logiques temporelles multi-agents”, Université Évry Val d'Essonne, Évry, France, September 2015.

  • C. Marché: examiner, PhD committee of Z. Chihani, “Certification of First-order proofs in classical and intuitionistic logics”, École Polytechnique, Palaiseau, France, November 2015.



previous Previous | up Home | Next next