Chargement...
 

Historique de fiche de formulaire


Version Date Utilisateur ID du Champ Champ Difference
5 178 Thesis advisor
-CONCHON Sylvain +ZAIDI Fatiha
      188 Co-advisors
-Fatiha Zaïdi +Sylvain Conchon
4 183 Objectives
 Pour cela, on utilisera le model checker Cubicle développé dans l'équipe Vals. Cubicle est basé sur une nouvelle technique de model checking qui repose sur la démonstration automatique SMT (Satisfiability Modulo Theories). Pour cela, on utilisera le model checker Cubicle développé dans l'équipe Vals. Cubicle est basé sur une nouvelle technique de model checking qui repose sur la démonstration automatique SMT (Satisfiability Modulo Theories).
 +Cubicle sera également utilisé par des techniques de génération de contre-exemple pour la génération de tests.
3 179 Subject
-Model Checking de programmes C11 avec Cubicle +Vérification par des techniques de test et model checking de programmes C11
      180 Abstract
 La norme C11 du langage C prend en charge la programmation avec threads sur architectures multi-coeurs. En particulier, elle introduit une notion de variables atomiques, ainsi qu'un système primitif de barrières de synchronisation (Acquire/Release fendes).  La norme C11 du langage C prend en charge la programmation avec threads sur architectures multi-coeurs. En particulier, elle introduit une notion de variables atomiques, ainsi qu'un système primitif de barrières de synchronisation (Acquire/Release fendes).
-Dans cette thèse, on s'intéressera à la vérification par model checking de programmes C11 avec threads pour des architectures à mémoire faible diverses. Pour cela, on utilisera le model checker Cubicle développé dans l'équipe Vals. Cubicle est basé sur une nouvelle technique de model checking qui repose sur la démonstration automatique SMT (Satisfiability Modulo Theories). +Dans cette thèse, on s'intéressera à la vérification par des techniques de test et model checking de programmes C11 avec threads pour des architectures à mémoire faible diverses. Pour cela, on utilisera le model checker Cubicle développé dans l'équipe Vals. Cubicle est basé sur une nouvelle technique de model checking qui repose sur la démonstration automatique SMT (Satisfiability Modulo Theories).
      184 Prerequisite
-Connaissances en model checking, démonstration automatique, compilation +Connaissances en test, model checking, démonstration automatique, compilation
2 181 Context
 La mise au point des programmes C concurrents est très difficile. Outre le non-déterminisme inhérent à ce style de programmation, le langage ne fournit pas assez d'information sur l'atomicité des opérations ou la gestion de la mémoire pour garantir la bonne exécution d'un programme contenant des threads. Ceci est d'autant plus aggravé par les modèles à mémoire faible des architectures modernes. La mise au point des programmes C concurrents est très difficile. Outre le non-déterminisme inhérent à ce style de programmation, le langage ne fournit pas assez d'information sur l'atomicité des opérations ou la gestion de la mémoire pour garantir la bonne exécution d'un programme contenant des threads. Ceci est d'autant plus aggravé par les modèles à mémoire faible des architectures modernes.
-La dernière norme C11 du langage C tente de remédier à cette situation en prenant en charge le multi-threading. En particulier, elle introduit une notion de variable atomiques, ainsi qu'un système primitif de barrières de synchronisation (Acquire/Release fences) pour écrire des programmes concurrents sur architectures multi-coeurs. +La dernière norme C11 du langage C tente de remédier à cette situation en prenant en charge le multi-threading. En particulier, elle introduit une notion de variables atomiques, ainsi qu'un système primitif de barrières de synchronisation (Acquire/Release fences) pour écrire des programmes concurrents sur architectures multi-coeurs.
1 180 Abstract
-La norme C11 du langage C prend en charge la programmation avec threads sur architectures multi-coeurs. En particulier, elle introduit une notion de variable atomiques, ainsi qu'un système de barrière de synchronisation primitif (Acquire/Release fendes). Dans cette thèse, on s'intéressera à la vérification par model checking de programmes C11 avec threads pour des architectures à mémoire faible diverses. Pour cela, on utilisera le model checker Cubicle développé dans l'équipe Vals. Cubicle est basé sur une nouvelle technique de model checking qui repose sur la démonstration automatique SMT (Satisfiability Modulo Theories). +La norme C11 du langage C prend en charge la programmation avec threads sur architectures multi-coeurs. En particulier, elle introduit une notion de variables atomiques, ainsi qu'un système primitif de barrières de synchronisation (Acquire/Release fendes). Dans cette thèse, on s'intéressera à la vérification par model checking de programmes C11 avec threads pour des architectures à mémoire faible diverses. Pour cela, on utilisera le model checker Cubicle développé dans l'équipe Vals. Cubicle est basé sur une nouvelle technique de model checking qui repose sur la démonstration automatique SMT (Satisfiability Modulo Theories).
      181 Context
-La mise au point des programmes C concurrents est très difficile. Outre le non-déterminisme inhérent à ce style de programmation, le langage ne fournit pas assez d'information sur l'atomicité des opérations ou la gestion de la modèle mémoire pour garantir la bonne exécution d'un programme contenant des threads. Ceci est d'autant plus aggravé par les modèles à mémoire faible des architectures modernes. +La mise au point des programmes C concurrents est très difficile. Outre le non-déterminisme inhérent à ce style de programmation, le langage ne fournit pas assez d'information sur l'atomicité des opérations ou la gestion de la mémoire pour garantir la bonne exécution d'un programme contenant des threads. Ceci est d'autant plus aggravé par les modèles à mémoire faible des architectures modernes.
-La dernière norme C11 du langage C tente de remédier à cette situation en prenant en charge le multi-threading. En particulier, elle introduit une notion de variable atomiques, ainsi qu'un système de barrière de synchronisation primitif (Acquire/Release fences) pour écrire des programmes concurrents sur architectures multi-coeurs. +La dernière norme C11 du langage C tente de remédier à cette situation en prenant en charge le multi-threading. En particulier, elle introduit une notion de variable atomiques, ainsi qu'un système primitif de barrières de synchronisation (Acquire/Release fences) pour écrire des programmes concurrents sur architectures multi-coeurs.

Ecole Doctorale Informatique Paris-Sud


Directrice
Nicole Bidoit
Assistante
Stéphanie Druetta
Conseiller aux thèses
Dominique Gouyou-Beauchamps

ED 427 - Université Paris-Sud
UFR Sciences Orsay
Bat 650 - aile nord - 417
Tel : 01 69 15 63 19
Fax : 01 69 15 63 87
courriel: ed-info à lri.fr