Chargement Évènements

« Tous les Évènements

  • Cet évènement est passé

EPIT 2015 École de Printemps d’Informatique Théorique « Preuve mécanisée de programmes »

24 mai 2015 @ 0 h 00 min - 29 mai 2015 @ 0 h 00 min

École de Printemps d’Informatique Théorique

« Preuve mécanisée de programmes »

du 24 au 29 mai 2015 à Fréjus

Cette école de printemps s’adresse à tous les jeunes chercheurs et chercheurs en informatique théorique souhaitant mieux comprendre ce qu’est un assistant de preuve et comment intégrer son usage dans sa recherche. Ainsi, aucune connaissance sur le domaine de la preuve sur ordinateur n’est nécessaire pour suivre cette école .

Les cours seront structurés en huit demi-journées (9h30 – 12h30 et 14h00 – 17h30). Une demi-journée comprendra un cours magistral d’une heure suivie (ou entrelacée) d’une séance de mise en pratique sur machine.

L’ensemble des supports pédagogiques et des logiciels seront disponibles sur une clé USB fournie à votre arrivée.

Les cinq premières demi-journées sont dédiées à la présentation des principaux concepts et techniques utilisés pour mécaniser des preuves sur ordinateur. On s’intéressera particulièrement aux raisonnements par induction, aux preuves d’algorithmes et programmes fonctionnels, impératifs et concurrents.

Les deux demi-journées suivantes porteront sur la mécanisation de deux domaines de l’informatique théorique : la théorie des langages rationnels et la combinatoire.

Enfin, lors de la dernière demi-journée, les participants réfléchiront à la mécanisation de leur propre domaine de recherche dans l’assistant de preuve Coq avec l’aide de l’équipe pédagogique de l’école.

Détails

Début :
24 mai 2015 @ 0 h 00 min
Fin :
29 mai 2015 @ 0 h 00 min
Catégorie d’évènement: