|
 
|
[DG13] Solveurs CP(FD) vérifiés formellement
Conférence Nationale avec comité de lecture : Neuvièmes Journées Francophones de Programmation par Contraintes (JFPC 2013), June 2013, pp.115-118, Aix-en-Provence,Mots clés: Vérification de programme - Solveurs de contraintes - Coq
Résumé:
Les solveurs de contraintes sont utilisés pour résoudre des problèmes d’optimisation, de planification,
d’ordonnancement, etc. Leur utilisation dans des domaines critiques réclame un certain degré de confiance et
requiert un examen sceptique des résultats fournis par un solveur, tout particulièrement lorsque ce dernier assure
qu’un problème n’a pas de solution. Nous proposons de développer un solveur pour les domaines finis - CP(FD)- correct par construction. Nous avons implanté le solveur à l’aide de l’outil de preuve Coq et l’avons prouvé
correct par rapport `a sa spécification elle-même exprimée en Coq. Il implante l’algorithme AC3 (et AC2001)
et met en œuvre une consistance d’arcs. Le mécanisme d’extraction de Coq permet d’obtenir un solveur écrit en
OCaml, formellement vérifié, le premier à notre connaissance. Ce solveur peut être utilisé pour résoudre un problème ou encore pour vérifier les résultats d’un autre solveur non vérifié formellement. Ces résultats ont été publiés récemmment dans les actes de la conférence internationale FM 2012.
Nous présentons ici un résumé de ces travaux et étudions leur extension à la consistance de bornes.
Equipe:
sys
BibTeX
| @inproceedings { | |||
| DG13, | |||
| title | = | "{Solveurs CP(FD) vérifiés formellement}", | |
| author | = | " C. Dubois and A. Gotlieb ", | |
| booktitle | = | "{Neuvièmes Journées Francophones de Programmation par Contraintes (JFPC 2013)}", | |
| year | = | 2013, | |
| month | = | "June", | |
| pages | = | "115-118", | |
| address | = | "Aix-en-Provence, ", | |
| } | |||
