Preuve formelle et contrainte alldiff

Session : SS10-2 / SS10 : Contraintes
Vendredi 12 février 15:00 - 16:00 Salle : RP13
Catherine Dubois, Antonin Butant et Sourour Elloumi

Nous nous intéressons à la vérification formelle de l'algorithme de filtrage (Régin 94) pour la contrainte alldiff. Cet algorithme utilise fortement la notion de couplage maximum. Nous présentons deux approches différentes de vérification formelle en Coq du calcul d'un couplage maximum dans un graphe.

Mots clés : Programmation par contraintes, contrainte alldiff, couplage maximum, preuve formelle, Coq