| 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). |