Projet de recherche doctoral numero :5127

Description

Date depot: 3 avril 2018
Titre: Combinaison d'Approches pour la Vérification Symbolique
Directeur de thèse: Yann THIERRY-MIEG (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini

Resumé: La vérification formelle de systèmes concurrents se heurte à des problèmes d'explosion combinatoire.La vérification symbolique propose de raisonner sur des ensembles, plutôt que sur des états individuellement considérés.Les stratégies de vérification symboliques sont nombreuses et hétérogènes. Les stratégies basées sur les diagrammes de décision réduits (BDD) permettent de représenter efficacement des grands ensembles. Les solvers SAT et SMT constituent un autre ensemble de stratégies de résolution pour ces problèmes.L'objectif du travail de thèse sera de développer des approches combinant ces solutions de façon efficace pour traiter des problèmes de model-checking.