Automatisation de la certification formelle de systèmes critiques par instrumentation d'interpréteurs abstraits

Les travaux menés dans cette thèse portent sur la certification de programmes. Les certificats établissent la validité des propriétés sémantiques des programmes. Ils sont produits sous forme de preuves déductives vérifiables par machine. Le défi relevé dans cette thèse est d'automatiser la construction des preuves de correction de programmes. Les propriétés sémantiques sont calculées par des analyseurs statiques de programmes qui s'appuient sur la théorie de l'interprétation abstraite. Nous proposons une méthode d'instrumentation des anaJyseurs statiques de programmes afin de leur faire générer automatiquement un certificat pour chaque propriété sémantique calculée. L'instrumentation consiste à associer à certaines fonctions d'un analyseur statique des patrons de preuve. De tels analyseurs instrumentés ne sont pas pour autant certifiés puisque leur correction pour toutes leurs entrées possibles n'est pas garantie. Cette approche permet de certifier avec un très haut-niveau de confiance les résultats d'outils existants, même à l'état de prototypes. Pour que l'instrumentation soit applicable en pratique, nous avons cherché à limiter le nombre de fonctions à instrumenter. Nous avons dégagé un ensemble restreint de fonctions, commun à tout analyseur, à instrumenter pour qu'un analyseur existant devienne un outil de certification. Nous avons appliqué cette technique d'instrumentation à un analyseur de programmes manipulant des tableaux et s'appuyant sur des domaines abstraits non triviaux. Cet analyseur calcule des propriétés sur le contenu des tableaux manipulés par les programmes et grâce à notre instrumentation il génère désormais des certificats vérifiables par Coq.This thesis deals with certification ofimperative program. Certificates establish validity of sorne semantics properties ofprograms. Certificates are machine-checkable formai proofs. The challenge raised in this thesis is to automatically generate correctness proofs of programs. We followed Floyd-Hoare method for proving that semantics properties are invariants and we used Coq system to check validity of proofs. We con si der that semantics properties are discovered by static analyzers based on abstract interpretation. We proposed to instrument static analyzers su ch that they automatically produce certificates of their results. Instrumentation consists in associating to sorne functions of an analyzer proof patterns which will generate the certificates at execution time. Such instrumented static analyzers are not certified because their correctness has not been established on all their input domain. Nevertheless they are able to justify by formai proofs that each of their results meet the specification. This framework offers the possibility to certify with a very high level of confidence the results of existing tools, even at the prototype stage. To make it practical we sought to restrict the number offunctions to instrument. We draw a limited set offunctions to instrument in order to transform any existing static analyzer in an automatic certification too\. We illustrate our instrumentation principle on an static analyzer that discovers invariants of array-processing programs. This analyzer uses nontrivial abstract domains on array programs content. Thanks to our instrumentation it produces Coq checkable certificates of discovered properties on arrays content.GRENOBLE1-BU Sciences (384212103) / SudocSudocFranceF