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...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | , , , , , , |
| Médium: | Thèse numérique |
| Jazyk: | Français Anglais |
| Vydáno: |
2022.
|
| Témata: | |
| On-line přístup: | 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 |
| Poznámka: |
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 |