Formalisation d'un vérificateur dynamique de propriétés mémoire pour programmes C
La vérification d'assertions à l'exécution est une technique permettant de contrôler, lors de leur exécution, la conformité d'un programme vis-à-vis d'une spécification donnée sous forme d'annotations formelles : les assertions. Un procédé appelé instrumentation transforme l...
Guardat en:
| Autor principal: | |
|---|---|
| Altres autors: | , , , , , , |
| Format: | Thèse numérique |
| Idioma: | Français Anglais |
| Publicat: |
2022.
|
| Matèries: | |
| Accés en línia: | Accès au texte intégral https://theses.univ-orleans.fr/public/2022ORLE1058_va.pdf http://www.theses.fr/2022ORLE1058/abes https://theses.hal.science/tel-04301178 |
| Nota: |
Titre provenant de l'écran-titre Ecole(s) Doctorale(s) : École doctorale Mathématiques, Informatique, Physique Théorique et Ingénierie des Systèmes (Centre-Val de Loire ; 2012-....) Partenaire(s) de recherche : Laboratoire d'informatique fondamentale d'Orléans (Orléans ; 1987-....) (Laboratoire) Autre(s) contribution(s) : Jean-Christophe Filliâtre (Président du jury) ; Jean-Christophe Filliâtre, Claude Marché, Julien Signoles, Nikolaï Kosmatov, François Pessaux (Membre(s) du jury) ; Alan Schmitt, Claude Marché (Rapporteur(s)) |
| Autres localisations: | Voir dans le Sudoc |
| Variante du titre: | Formalization of a Runtime Assertion Checker for Memory Properties of C Programs |