Fils d'Ariane

University : Main content

Titre de page

Soutenance de thèse de Dara LY

Contenu de la page principale

sefco_code_informatique

Date -
Heure 14h00 - 17h00
Adresse

Salle : LISN - Bâtiment DIGITEO - 1 rue Raimond Castaing et rue René Thom
91190 GIF SUR YVETTE
Francia

Contact
Lien http://www.univ-orleans.fr/fr/univ/recherche/temps-forts/soutenances-de-theses-…

La vérification d'assertions à l'exécution est une technique permettant de contrôler, lors de l'exécution d'un programme, la conformité de ce programme vis-à-vis d'une spécification donnée sous forme d'annotations formelles : les assertions. Un procédé appelé instrumentation transforme les assertions en code exécutable, de manière à mettre en œuvre un moniteur en ligne pour le programme à vérifier. Le long de l'exécution du programme instrumenté, le moniteur contrôle la conformité du programme vis-à-vis des assertions, et, en cas de non-respect d'une assertion, met fin à l'exécution. Autrement, il laisse le comportement fonctionnel du programme inchangé. La complexité de mise en œuvre de l'instrumentation dépend largement des propriétés exprimables dans le langage d'annotation. Dans le cas de programmes en langage C, l'outil E-ACSL (greffon de Frama-C, une plateforme open-source d'analyse de code C), permet la vérification de propriétés relatives à l'état mémoire du programme, mais requiert pour cela une instrumentation complexe. La présente thèse est consacrée à la formalisation de cette instrumentation : il s'agit d'en donner une définition précise et d'étudier ses propriétés sémantiques. Nous proposons une modélisation du problème comme une traduction de programmes depuis un langage source, muni d'assertions logiques, vers un langage cible. Ce dernier est dépourvu d'assertions logiques, mais intègre une structure de données, appelée mémoire d'observation, dédiée au suivi des propriétés mémoire. Nous donnons une caractérisation axiomatique de la mémoire d'observation, et utilisons celle-ci pour définir la sémantique du langage cible de la transformation, dont nous montrons qu'elle est correcte vis-à-vis de la sémantique des langages concernés. Additionnellement, nous étudions l'optimisation de l'instrumentation par analyse de flot de données, technique mise en œuvre dans l'outil E-ACSL afin de réduire le surcoût en performance induit par l'instrumentation. L'analyse vise à déterminer un sous-ensemble d'emplacements mémoire minimal dont l'instrumentation permette au moniteur d'évaluer correctement les assertions du programme. Nous définissons une telle analyse, et prouvons qu'elle est sûre, au sens où limiter l'instrumentation aux seuls emplacements désignés par l'analyse ne compromet pas la validité des verdicts du moniteur.