Nicolas Magaud Maître de conférences, Université de Strasbourg Département d'Informatique Equipe Informatique Géométrique et Graphique Equipe-Projet INRIA Camus LSIIT, UMR 7005 CNRS-ULP Pôle API, Bd Sébastien Brant - BP 10413 67412 ILLKIRCH CEDEX - FRANCE Courriels/E-mails: magaud @ unistra.fr nicolas.magaud @ ens-lyon.org Pôle API: Bureau C118 - Tel: (+33) 3 68 85 45 61 DI, Esplanade: Bureau 306 - Tel: (+33) 3 68 85 02 46 Fax: (+33) 3 68 85 44 55 (Pôle API)

Mobilitétudiante

Propositions de stages et de sujets de TER

• Prouveur automatique de relations d'incidence (en collaboration avec avec Julien Narboux et Pascal Schreck)
• Génération automatique de contre-exemples (en collaboration avec Julien Narboux)
• Symétrie des preuves (en collaboration avec Julien Narboux)
• Preuve en Coq du théorème de Pick (en collaboration avec Julien Narboux)
• Traduction de spécifications algébriques vers Prolog et Coq (en collaboration avec Pascal Schreck)
• Formalisation de la sémantique dénotationnelle et du théorème de Scott-Tarski en Coq (en collaboration avec Pascal Schreck)

• Coordinateur des réunions des opérations 2 et 3 de l'équipe IGG (sept. 2007- sept. 2011)
• ANR Project Galapagos: Géométrie, Algorithmes et Preuves (dec. 2007 - oct. 2011)
  • Co-encadrement de la thèse de Christophe Brun dirigée par Jean-François Dufourd (2007-2010, thèse soutenue le 06/12/2010)
• Membre du comité de programme des Journées francophones des langages applicatifs (JFLA'08)
• Formal Proofs in Geometry
• Specifications, Proofs and Verification of Imperative Programs
• Type Theory, Data Representations and Proof Transformations
• Proof-Carrying Code and Machine-Independent Code Certification
• Publications

  CDR: A tool to help changing data representations in Coq (2006)

• CDR is a tool designed to make Changing Data Representation easier in a type-theory based proof assistant like Coq.

Vulgarisation

• Un aspect de l'ingénierie et du logiciel : la fiabilité du logiciel (présenté aux journées des Universités - 8 mars 2008)

Activités d'Enseignement (Teaching)

• Premier semestre 2011-2012
  • ENSIIE Strasbourg : Algorithmique et Programmation (IAP 1)
  • ENSIIE Strasbourg : Validation et Vérification du Logiciel (partie : Logique de Hoare et Frama-C)
  • L2-Info : Structures de données et algorithmes 2
  • L3-Math: Algorithmique et Structure de Données (CC (2005/2006), CC (2006/2007), examen (2006/2007), CC (2007/2008), examen (2007/2008))
  • M2-ISI: Preuve et certification logicielle
  • L2-APE2
• Second semestre 2011-2012
  • M1-Info : Ingénierie de la Preuve (qq ressources)
  • M1-ChemoInformatique : Génie logiciel
  • L1-MathInfo : APE 1

Charges administratives

• Correspondant de la Direction des Relations Internationales de l'Université de Strasbourg pour le Département d'Informatique (depuis 2009)
• Coordinateur pour les enseignements d'APE (APE1 en L1-mathinfo, APE2 en L2-info) pour le département d'Informatique (depuis 2011)
• Coordinateur des interventions de l'ULP puis de l'Université de Strasbourg dans les lycées d'Alsace pour le département d'informatique (2006-2010)

Misc.

• Vice-président de l'association ASCPA, en charge de la section escalade (depuis 2008)
• Président du Comité départemental 67 de la FFME, membre élu du Comité Régional Alsace de la FFME (depuis 2009)

• Scuba diving: CMAS ***, PADI Rescue+Deep+Nitrox.
• North West Island(2 weeks there in Dec. 04 with the UNSW Underwater club).
• Changer d'approche , Expédition Vanikoro, Laperouse 2005, Santo 2006