Tools and Techniques for the Verification of Modular Stateful Code
Parreira Pereira, Mário José · 2018
Cette these se place dans le cadre des methodes formelles et plus precisement dans celui de la verification deductive et du systeme Why3. Ce dernier fournit un ensemble d'outils pour la specification, l'implementation et la verification a l'aide de demonstrateurs externes. Why3 propose en particulier un langage de programmation adapte a la preuve, appele WhyML. Un aspect important de ce langage est le code fantome, a savoir des elements de programme introduits exclusivement pour les besoins de la specification et de la preuve. Pour obtenir un code executable, le code fantome est elimine par un processus automatique appele extraction. L'une des contributions principales de cette these est la formalisation et l'implementation du mecanisme d'extraction deWhy3. La formalisation consiste a montrer que le programme extrait preserve la semantique du programme de depart, en s'appuyant notamment sur un systeme de types avec effets. Ce mecanisme d'extraction a ete utilise avec succes pour obtenir plusieurs modules OCaml corrects par construction, dans le cadre d'une bibliotheque verifiee de structures de donnees et d'algorithmes. Cet effort de preuve a conduit a deux autres contributions de cette these.La premiere est une technique systematique pour la verification de structures avec pointeurs, a l'aide de modeles du tas delimites.Une preuve entierement automatique d'une structure union-find a pu etre obtenue grâce a cette technique. La seconde contribution est un moyen de specifier un algorithme d'iteration independamment de son implementation. Plusieurs curseurs et iterateurs d'ordre superieur ont ete specifies et verifies en utilisant cette approche.