Automated verification of heap-manipulating programs with infinite data

Le developpement de techniques rigoureuses et automatiques pour la verification des systemes logiciels est une tâche importante. Cette these porte sur la verification des proprietes de surete pour des programmes avec memoire dynamique et donnees infinies. Elle developpe un cadre base sur la logique ou les specifications des programmes sont donnees par des formules. Premierement, nous considerons l'automatisation du raisonnement pre/post-condition. Nous definissons une logique, appelee CSL, pour la specification des structures chainees ou des tableaux, ainsi que des compositions de ces structures. Les formules CSL decrivent des relations d'accessibilite entre les cellules de memoire, la taille du tas et les donnees scalaires. Nous prouvons que le probleme de la satisfiabilite pour CSL est decidable et que CSL est fermee par le calcul de la post-condition. Ensuite, nous considerons la synthese automatique d'assertions pour des programmes avec des listes simplement chainees. Un cadre base sur l'interpretation abstraite est defini qui combine une abstraction finie sur la forme du tas avec une abstraction sur des sequences de donnees. Les abstractions sur les sequences permettent de raisonner sur leurs tailles, les multi-ensembles de leurs elements, ou les relations entre leurs donnees a des differentes positions. Nous definissons une analyse inter-procedurale qui calcule l'effet de chaque procedure de facon locale sur la partie du tas accessible a partir de ses parametres. Ces techniques sont implantees dans un outil qui montre que notre approche est assez puissante pour la generation automatique de resumes de procedure non-triviales et le raisonnement pre/post-condition.