Abstract FR:

Le travail de these concerne la verification formelle de programmes imperatifs. Dans ce domaine, les outils developpes jusqu'a present portent sur des proprietes tres generales et requierent le plus souvent une bonne connaissance par l'utilisateur de la logique sous-jacente. La demarche adoptee consiste a appliquer des techniques d'analyse statique a des classes de proprietes plus restreintes, utiles a la mise au point de programmes. Cette approche nous permet d'obtenir une automatisation plus importante et d'alleger ainsi la tache du developpeur. Nous nous sommes focalises sur des proprietes de connexite entre pointeurs qui permettent de verifier la correction des references a des adresses de la memoire. L'intervention de l'utilisateur est cependant souhaitable lors d'une session de mise au point, notamment pour lever certaines ambiguites dues aux approximations inherentes a une analyse statique. Nous introduisons donc une forme d'interaction avec l'utilisateur qui est integree dans l'outil sous la forme d'annotations de programmes. Ces annotations sont prises en compte de maniere naturelle par l'analyseur et ne demandent pas de la part du developpeur une grande expertise sur la theorie sous-jacente. Les resultats theoriques sont valides par la mise en uvre d'un prototype qui permet de tester les performances en terme d'efficacite et de precision de l'outil.