Loading...
 
[Show/Hide Left Column]

Sujets Help

Print History View Items
No Tabs
ViewCommentsAttachments (0)

View Item

Domain Programming-Testing-Proving
Domain - extra
Year 2014
Starting 01/10/2014
Status Open
Subject Vérification par des techniques de test et model checking de programmes C11
Thesis advisor ZAIDI Fatiha
Co-advisors Sylvain Conchon
Laboratory LRI VALS
Collaborations
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 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).
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 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.
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).
Cubicle sera également utilisé par des techniques de génération de contre-exemple pour la génération de tests.
Work program
Extra information
Prerequisite Connaissances en test, model checking, démonstration automatique, compilation
Details
Expected funding Institutional funding
Status of funding Expected
Candidates David Declerck
user sylvain.conchon
Created Monday 19 of May, 2014 22:57:18 CEST
LastModif Friday 06 of June, 2014 17:53:14 CEST


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