Le sujet de thèse s'inscrit dans le cadre de la preuve formelle de programmes C telle que pratiquée au sein de la plateforme Frama-C développée par notre laboratoire.
Pour faciliter les raisonnements sur des programmes manipulant des structures de données de plus en plus complexes, nous avons besoin de développer un nouveau modèle mémoire qui permette de décrire et d'identifier des régions de la mémoire ayant de bonnes propriétés (validité, séparation, type d'accès, etc.).
Ce nouveau modèle mémoire est suffisamment complexe pour qu'il soit nécessaire d'en assurer la cohérence et la correction.
Le candidat devra formaliser ce modèle et sa sémantique et prouver sa correction en utilisant l'assistant de preuve Coq et des techniques de logique de séparation.
Date de début souhaitée : 01-10-
Directeur de thèse : LOULERGUE Frédéric
Organisme : Université d'Orléans
Laboratoire : Laboratoire d’Informatique Fondamentale d’Orléans (LIFO)
#J-18808-Ljbffr
En cliquant sur "JE DÉPOSE MON CV", vous acceptez nos CGU et déclarez avoir pris connaissance de la politique de protection des données du site jobijoba.com.