Thorie de Test Des Programmes Contraintes

Le dveloppement des langages de modlisation des programmes contraintes a eu un grand impact dans le monde industriel comme OPL de IBM Ilog, Comet de Dynadec, Sicstus Prolog ou Gecode qui proposent des solutions robustes aux problmes du monde rel. De plus, ces langages commencent tre utiliss dans des applications critiques comme la gestion et le contrle du trafic arien, le e-commerce et le dveloppement de programmes critiques. D'autre part, il est connu que tout processus de dveloppement logiciel effectu dans un cadre industriel inclut imprativement une phase de test, de vrification formelle et/ou de validation. Par ailleurs, ces langages ne connaissent pas d'innovations majeures en termes de vrification et de mise au point. Ceci ouvre la voie des recherches orientes vers les aspects gnie logiciel ddis la PPC (programmation par contraintes). Le travail majeur de cette thse pose les jalons d'une thorie du test des programmes contraintes ainsi qu'un cadre conceptuel pour la mise-au-point de ce type de programmes avec une mthodologie de localisation et de correction automatique.