Abstract FR:

Le systeme typique de verification de programmes accepte en entree un programme annote avec des assertions a la floyd-hoare et genere en sortie une liste de conditions de verification. Malheureusement, le systeme ne peut pas relier un echec dans la preuve d'une condition a une position dans le programme ou dans les assertions. Nous apportons une reponse a ce probleme en proposant l'integration de plusieurs facilites dans un systeme de verification. Le tracage des origines a pour role d'annoter les conditions generees avec leurs origines dans le programme source. Il repose sur une instrumentation du generateur de conditions avec un calcul d'origines. L'instrumentation est systematique etant dirigee par la forme syntaxique des regles. Nous prouvons la correction du generateur instrumente et que sa complexite est un facteur constant de celle du generateur initial. Une implantation de cette technique a ete realisee dans le systeme centaur. Les coupes de programme peuvent fournir des informations plus precises en isolant l'ensemble des instructions qui affectent la validite d'une assertion. Le calcul de ces coupes passe lui aussi par une instrumentation du generateur qui se charge de tracer les dependances entre les conditions et le programme. Comme le tracage des origines, cette methode est purement syntaxique et donc generique. L'analyse des coupes obtenues montre qu'elles capturent bien les dependances de donnees, mais pas celles de controle. Cela nous amene a etudier les dependances induites par les assertions dans un programme annote. Nous montrons qu'un calcul simplifie des conditions de verification peut se faire directement sur le graphe de dependances. L'analyse de dependances nous permet egalement de propager les assertions dans un programme annote. Nous concluons par une etude de cas en b portant sur la verification de l'algorithme de kruskal pour la recherche d'un arbre de recouvrement minimal. Elle se distingue des applications habituelles de la methode b par la complexite des algorithmes employes et l'utilisation de structures de donnees evoluees. Le developpement par raffinements successifs nous permet de decomposer la verification en plusieurs etapes allant de la specification jusqu'a l'implantation.