Présentation de la mention
| Вид материала | Документы |
СодержаниеResponsable : Thérèse HARDIN |
- A few slides from the Presentation, 31.45kb.
- На русском и английском языках, 160.31kb.
- Стандарт університету, 259.5kb.
- International Communist Seminar (Brussels) Presentation Международный Коммунистический, 29.1kb.
| Acronyme : sct | Spécialité : STL | 3 ECTS | Niveau : 500 | Semestre : S3 |
| Titre : Spécification et certification en théorie des types | ||||
| Responsable : Thérèse HARDIN | Répartition hebdomadaire ou semestrielle | |||
| (30h/7 semaines) | ||||
ContenuCette UE a pour objectif l'étude des théories des types qui fondent les langages de spécification formelle et les méthodes de preuve de correction du logiciel. Une place importante est réservée à l'étude des propriétés logiques et mathématiques de ces théories. La manipulation de différents systèmes d'aide à la preuve permet de comprendre leur mise en oeuvre. Enfin, leur utilisation dans les outils de compilation ou d'édition de liens sont aussi présentées. | ||||
Expérience du responsable dans le domaine de l’UEQuelques thèmes de recherche de T. Hardin, accompagnés de quelques publications: Compilation et sémantique ( Hardin, Properties of CCL, TCS, 1989, Explicit substitutions properties, Curien, Hardin, Lévy, JACM 1996, Hardin,Maranget, Pagano,Functional runtime systems, J. of Functional Programming, 1998,T. Hardin, Mammass,Proving the Bounded Retransmission Protocol in the Pi-calculus, NFINITY'98 ). Logique et démonstration automatique (Dowek,Hardin,Kirchner, Higher-order unification via explicit substitutions, Information and Computation,2000; Theorem Proving modulo, Journal of Automated Reasoning,2003). Responsable du projet FOCAL, atelier de développement de systèmes répondant aux besoins élevés de sûreté et de sécurité (Dubois,Hardin, Viguié, Building certified components within FOCAL,Trends in Functional Programming,2004; ia.fr), utilisé dans 3 ACI Sécurité (Modulogic, Edemoi, Alidecs). Sûreté de fonctionnement (P. Ayrault, T. Hardin, Développement d'un outil d'évaluation de la sûreté du logiciel, JFLA2000, Hardin, Logiciels de confiance, JFLA2002). Quelques thèmes d'enseignement de T. Hardin, correspondant à des cours de niveaux L et M: Programmation (Hardin , V. Viguié-Donzeau, Concepts et outils de programmation, avec Caml et Ada, InterEditions1992), Lambda-calculs, Théorie des types, Réécriture, Sémantiques, démonstration automatique, Sûreté de fonctionnement (Normes, méthodes de mise en oeuvre, méthodes d'évaluation), accent mis sur tous les aspects liés au logiciel embarqué, en particulier sur les méthodes formelles. | ||||
Réalisations du responsable dans le domaine de l’UE
| ||||