Écrire des programmes prouvés corrects avec Coq Garantir mathématiquement le respect d'une spécification programmation coq méthodes formelles
Introduction à la preuve de programmes C avec Frama-C et son greffon WP Introduction à la spécification et la preuve de programmes C, par l'usage de Frama-C, du langage ACSL et son greffon WP. Quelques rudiments théoriques sont donnés. c méthodes formelles preuve déductive
Un zeste de mathématiques assistées par ordinateur Quand la machine vient en support du mathématicien mathématiques coq méthodes formelles
