Loading...
 
[Show/Hide Left Column]

Tracker Item History Help

Close
warningNot logging
Tracker changes are not being logged: Go to Action log admin to enable

Version Date User Field ID Field Old New
5 14:07 178 Thesis advisor CONCHON Sylvain ZAIDI Fatiha
5 14:07 188 Co-advisors Fatiha Zaïdi
Sylvain Conchon
4 14:07 183 Objectives L'objectif de cette thèse est la vérification formelle de propriétés de sûreté de programmes C11 par model checking. Cette technique de vérification tente de vérifier la sûreté d'un programme concurrent en explorant (statiquement) tous ses comportements possibles à l'exécution.

En particulier, on s'intéressera à garantir la non-atteignabilité d'états indésirables pour des programmes faisant intervenir un nombre quelconque de threads et/ou basés sur 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).

L'objectif de cette thèse est la vérification formelle de propriétés de sûreté de programmes C11 par model checking. Cette technique de vérification tente de vérifier la sûreté d'un programme concurrent en explorant (statiquement) tous ses comportements possibles à l'exécution.

En particulier, on s'intéressera à garantir la non-atteignabilité d'états indésirables pour des programmes faisant intervenir un nombre quelconque de threads et/ou basés sur 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).
Cubicle sera également utilisé par des techniques de génération de contre-exemple pour la génération de tests.

3 14:07 179 Subject Model Checking de programmes C11 avec Cubicle
Vérification par des techniques de test et model checking de programmes C11
3 14:07 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).
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 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).
3 14:07 184 Prerequisite Connaissances en model checking, démonstration automatique, compilation
Connaissances en test, model checking, démonstration automatique, compilation
2 14:07 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 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 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 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 14:07 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).
1 14:07 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 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 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.

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 at lri.fr