Abstract FR:

Le probleme aborde dans cette these concerne la production automatique de donnees de test permettant de prouver des proprietes de programmes. Nous nous situons ainsi a mi-chemin entre le domaine du test et celui de la verification de programmes. Les travaux dans le domaine du test ont conduit a des outils semi-automatiques d'utilisation simple, mais qui reposent sur des hypotheses difficilement verifiables en pratique. Dans le domaine de la verification, des outils bases sur des methodes formelles ont ete developpes, mais ils necessitent un utilisateur expert dans les techniques de preuve utilisees par l'outil. Cette situation est due aux problemes d'indecidabilite engendres par la puissance des formalismes traites. La these que nous presentons est qu'il est possible de developper des methodes formelles automatiques pour prouver des proprietes de programmes, a condition de considerer des formalismes restreints. Notre principale contribution est une nouvelle approche pour la verification de programmes, integrant les techniques de test et d'analyse statique. Nous proposons une methode formelle de generation de jeux de test finis complets permettant de prouver qu'un programme verifie une propriete donnee. Cette methode utilise le texte du programme et de la propriete, qui doivent appartenir a certaines classes de programmes (ou de proprietes). Ces classes sont representees par des hierarchies de schemas, qui peuvent etre vues comme modelisant des hypotheses de test. Pour une propriete donnee, notre methode est completement automatique et ne necessite donc aucune competence particuliere de l'utilisateur. Tout programme appartenant au schema et passant le jeu de test avec succes verifie la propriete testee. Nous avons implante cette methode dans un prototype (traitant un langage fonctionnel restreint), pour le cas de proprietes s'exprimant en termes de longueur de liste.