Solveurs CP(FD) vérifiés formellement

International audienceLes 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 etrequiert un examen sceptique des résultats fournis par un solveur, tout particulièrement lorsque ce dernier assurequ?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 enOCaml, 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