EN FR

Contact

pierre.courtieu@cnam.fr

Position

Je suis maître de conférences au CNAM Paris depuis 2005. Dans l’équipe SYS du laboratoire Cédric. Je suis actuellement le chef d’équipe (tournant) de l’équipe SYS.

• page officielle de l’équipe SYS
• lien utiles pour les membres
• Ma page Labo
• Séminaire de l’équipe SYS.

Par ailleurs

• J’ai été (1er sept 2014-31 août 2016) en délégation dans l’équipe Gallium (devenue Cambium) de l’INRIA.
• j’ai été en CRCT (congé pour recherche) dans l’équipe Proval du LRI, du 1er octobre 2012 au 31 mars 2013

Recherche

Je m’intéresse à la preuve formelle et/ou automatique et en particulier à la preuve de programmes. En particulier avec l’assistant de preuve Coq.

• L’introduction de ma thèse
• Mon poly de preuve de programme
• Publications
• Coq

Projects financés actuels

• ANR Générique SAPPORO(2019-CE25-0005-1)
  Offres de stage (M2) et thèses
  • MODEL VALIDATION FOR LUMINOUS ROBOTS précision prolongeable en thèse
  • CERTIFICATION OF ALGORITHMS FOR (NON-EUCLIDEAN) GEOMETRY précision prolongeable en thèse
  • PROOF AUTOMATION IN GRAPHS AND SWARMS précision prolongeable en thèse
  • RANDOMIZED PROTOCOLS AND THEIR CERTIFICATION précision prolongeable en thèse ## Anciens projets

Enseignement

Informations pratiques

• Plan du Cnam
• Accéder au Cnam
• Programmer ses inscription au CNAM - mode d’emploi du site du CNAM

cours

• DIU EIL

  • Calendrier session 1
  • moodle

• NFA031

• NFA035

• Master M2IF – option Automated Deduction, and opening to Distributed Algorithms”

  • Slides
  • Tutoriel coq

• Master SEMS

  • Page du master SEMS

• ENSIIE Transparents de Calculabilité:

  • compressés
  • non compressés
  • complet (avec overlays)

Développements

• Some emacs stuff
• Une calculette à bande
• inout.{h,c} une librairie C d’entrée sortie simplifiées pour les débutants.

Libraries Coq

• LybHyps (auteur: Pierre Courtieu) un développement permettant la manipulations des hypothèses en Coq. Écrit en Ltac, il permet d’appliquer une tactique à toutes les nouvelles hypothèses après l’application d’une tactique. En particulier un renommage automatique et customisable des hypothèses.

• Sparkformal (Zhi Zang, Pierre Courtieu) A semantic for a subset of the Spark programing language. The archive also include the textual semantic in Z format of Spark written in 1983 (author Ian O’Neill and William March).

• SparkCompcert (Pierre Courtieu) Spark frontend for CompCert (work in progress), based on Sparkformal above is the most up to date. Based on and dependening on the semantic above.

• loglangcoq (Pierre Courtieu, Julien Forest, Olivier Pons) Un développement Coq sur la logique propositionnelle et de premier ordre, ainsi que la sémantique des langage de programmation. Des preuves sur la méthode des tableaux et une preuve de complétude de la déduction naturelle notamment. Résultat visible là.

• PMachine (Tristan Crolard, Maria-Virginia Aponte, Julia Lawall, Pierre Courtieu) Un développement Coq formalisant une partie du fonctionnement de la P-machine pour un mini langage à la SPARK et utilisant le plugin de Marc Lasson pour prouver l’équivalence entre deux implémentations de la pile d’appel des procédures. La présence de procédures imbriquées est laprincipale difficulté ici, ainsi que labsence de clôture.

• ProofGeneral ProofGeneral, emacs mode for Coq (David Aspinal, Paul Steckler, Erik Martin-Dorel, Pierre Courtieu, Hendriks Tews).

• Pactole Coq Framework for proving distributed protocols for autonomous robots. Some non trivial protocoles together with impossibility proofs.