Contributions à la génération de tests à base de contraintes

These last years have seen the development of several constraint solving techniques dedicated to the testing of software systems, in an area called ''Constraint-Based Testing''. Our approach in this research domain consists to explore how Constraint Programming techniques can help the automatic generation of tests for imperative programs. We have addressed hard combinatorial problems resulting from automatic test cases generation by developing constraint propagation and filtering techniques well-tuned for handling control and data structures of imperative programs. Our habilitation tries to establish a first synthesis of the domain through five contributions, namely hybrid constraint solving for automatic test case generation, probabilistic test generation through probabilistic constraint combinator, constraints over abstract memory models, constraint solving over floating-point expressions and testing of constraint programs. We also illustrate these contributions through their application to critical software verification, and draw several research perspectives to our work.Ces dernières années, les recherches en matière de Test Logiciel ont conduit au développement de techniques de résolution de contraintes dédiées, dans ce qui est appelé ''le test à base de contraintes''. Notre approche dans ce domaine vise à explorer l'apport de la Programmation par Contraintes à la génération automatique de test pour les programmes impératifs. Nous nous sommes intéressés à la résolution de problèmes combinatoires difficiles issus de la génération de données de test, en développant des techniques de propagation de contraintes et de filtrage, adaptées au traitement des constructions des langages de programmation. Notre habilitation tente de faire une première synthèse de ce sujet au travers de cinq contributions: l'hybridation de techniques de résolution de contraintes pour la génération automatique de cas de test, la génération probabiliste de cas de test à l'aide d'opérateurs à contrainte probabiliste, les contraintes sur un modèle mémoire pour les programmes manipulant les pointeurs, la résolution de contraintes sur les expressions portant sur les nombres à virgule flottante, et le test de programmes à contraintes. Nous illustrons également ces contributions par leur application à la vérification de logiciels critiques, et dressons quelques perspectives à ces travaux