Y. Bertot

Preuve et programmation fiable

L'objectif de ce cours est de décrire comment produire des programmes entièrement corrects vis-à-vis de spécifications logiques en utilisant le système de preuve Coq.

S3 3 ECTS 24h OPT Site web yves.bertot@inria.fr