Qui sommes-nous ?
Espace utilisateur
Formation continue
Credit : L. Godart/CEA
D’un jour à plusieurs semaines, nos formations permettent une montée en compétence dans votre emploi ou accompagnent vers le retour à l’emploi. 
Conseil et accompagnement
Crédit : vgajic
Fort de plus de 60 ans d’expériences, l’INSTN accompagne les entreprises et organismes à différents stades de leurs projets de développement du capital humain.
Thèses
Accueil   /   Post Doctorat   /   Conception de techniques de compilation pour améliorer l'efficacité d'E-ACSL, un vérificateur d'assertions à l'exécution pour programmes C

Conception de techniques de compilation pour améliorer l'efficacité d'E-ACSL, un vérificateur d'assertions à l'exécution pour programmes C

Cybersécurité : hardware et software Défis technologiques Informatique et logiciels Sciences pour l’ingénieur

Résumé du sujet

Notre équipe développe Frama-C (http://frama-c.com), une plateforme d'analyse de programmes C qui fournit plusieurs analyseurs sous forme de greffons. Frama-C lui-même est développé en OCaml. Cette plateforme permet à l'utilisateur d'annoter des programmes C à l'aide de spécifications formelles écrites dans le langage ACSL. Elle peut ensuite garantir qu'un programme C satisfait sa spécification à l'aide de techniques formelles comme l'interprétation abstraite, la preuve de programmes ou la vérification à l'exécution. E-ACSL est ainsi le greffon de Frama-C en charge de la vérification à l'exécution. Il convertit un programme C annoté avec des annotations formelles en un nouveau programme C qui vérifie la validité des annotations pendant l'exécution du programme: par défaut, l'exécution est arrêtée dès lors qu'une annotation est violée. S'il n'y a pas d'erreur, le programme s'exécute normalement. Une caractéristique importante d'E-ACSL est l'expressivité de son langage de spécification qui permet de décrire de nombreuses propriétés de sûreté et de sécurité. Une autre caractéristique importante est l'efficacité du code généré qui repose notamment sur une bibliothèque et des analyses statiques dédiées. Cependant, E-ACSL peut encore être amélioré sur de nombreux points pour étendre l'expressivité, tout en réduisant les temps d'exécution et la consommation mémoire. C'est l'objectif du post-doctorat.

Laboratoire

Département Ingénierie Logiciels et Systèmes (LIST)
LSL (DILS)
Laboratoire pour la Sûreté du Logiciel
Top envelopegraduation-hatlicensebookuserusersmap-markercalendar-fullbubblecrossmenuarrow-down