Abstract FR:

La verification des programmes a pour objectif de garantir la conformite des programmes avec leur specification. Cette activite prend des formes variees selon le langage de programmation utilise, la nature de la specification, et ce que l'on entend par conformite. Cette these est consacree a l'etude de methodes de preuves formelles pour les programmes logiques avec negation. Notre approche est declarative, c'est-a-dire que la semantique des programmes est donnee en termes purement logiques. Nous etudions principalement deux methodes. La premiere a pour but de demontrer des proprietes du modele bien-fonde. La technique proposee consiste a representer ces proprietes sous forme de d'annotations, ce qui facilite l'organisation et accroit la modularite des preuves. La seconde methode utilise une procedure a base de depliage. Elle permet de demontrer des proprietes vraies dans tous les modeles du complete. Ces methodes ont en pratique des atouts et des limitations de nature differente. La possibilite et l'interet qui resulte de leur combinaison, ainsi que le support d'outils automatiques, montrent une voie prometteuse vers la mise en uvre de preuves a plus grande echelle. Ce travail contribue a promouvoir l'interet de la programmation en logique pour le genie logiciel