Groupe de travail VERIFICARD
Claude Marché, Christine Paulin, Xavier Urbain
Présentation
L'objectif de ce groupe de travail est de définir une méthode de
représentation dans Coq de programmes écrits dans un
(sous-ensemble) de Java. Cette représentation doit permettre à partir
d'une spécification du programme d'engendrer un ensemble d'obligations
de preuve qui pourront être vérifiées par Coq.
Ce travail s'insère dans le cadre du projet européen
VERIFICARD.
Prochains groupes de travail
Mercredi 13 novembre, 10h--12h, salle 90
Atelier pratique KRAKATOA/WHY.
Groupes de travail passés
Mercredi 30 octobre, 14h--16H, salle 90
Mercredi 2 octobre, 10h--12h, salle 90
JCF : Rien d'exceptionnel.
Mercredi 11 septembre, 13h--16h30, salle Firtech
KRAKATOA.
Mercredi 5 juin, 10h--12h, salle 101
Mercredi 22 mai, 10h--12h, salle 79 Nicolas Oury : Modifications en place.
Mardi 7 mai, 10h--12h, salle 101
Mercredi 3 avril, 10h--12h, salle 101 Exemples traités par
KRAKATOA et WHY.
Mercredi 20 mars, 10h--12h, salle 101 Présentation du proto WHY.
Mercredi 6 mars, 10h--12h, salle 101 Présentation de la
modélisation.
Mercredi 16 janvier, 10h--12h, salle Firtech Xavier :
Compte-rendu du meeting Verificard.
Mercredi 12 décembre, 10h--12h, salle Firtech JCF :
porte-monnaie électronique.
Mercredi 5 décembre, 10h--12h, salle Firtech Christine :
The Loop Compiler for Java and JML de van den Berg & Jacobs ;
JCF : JML ;
Mercredi 28 novembre, 10h--12h, salle Firtech Xavier : sémantique opérationnelle à la Börger
& Schulte ;
Mercredi 21 novembre, 10h--12h, salle 148 Claude : BALI ;
Mercredi 14 novembre, 10h--12h, salle 101 Claude : BALI ;
Jeudi 8 novembre, 10h--12h, salle 101 Xavier : le système JIVE.
This document was translated from LATEX by
HEVEA.