Informations professionnelles
Statut: Docteur ED
ED: EDITE
Unité de recherche: LIP6
Employeur: EPITA Date de debut de thèse: 7 octobre 2019 Date soutenance de thèse: 19 décembre 2023 Encadrant : Etienne RENAULT (LRE) Directeur de thèse: Souheib BAARIR (LIP6) Sujet de thèse: Parallélisations et optimisations du Bounded Model-checking
Employeur: EPITA Date de debut de thèse: 7 octobre 2019 Date soutenance de thèse: 19 décembre 2023 Encadrant : Etienne RENAULT (LRE) Directeur de thèse: Souheib BAARIR (LIP6) Sujet de thèse: Parallélisations et optimisations du Bounded Model-checking
Soutenance de thèse
Données générales
Titre : Contribution to SAT-based Bounded Model Checking
Date : 19 décembre 2023
Heure: 10:00
Résumé : Cette thèse se concentre sur l'extraction d'informations de haut niveau qui caractérisent les problèmes de vérification de modèle bornée (BMC) dans le but d'identifier et/ou de construire des clauses pertinentes, permettant la suppression efficace des sous-espaces inutiles en injectant ces clauses dans le solveur SAT. La thèse propose diverses techniques orthogonales à cette fin pour améliorer les performances des procédures SAT dans l'évaluation des instances BMC, aussi bien dans des contextes séquentiels que parallèles. Trois axes d'exploration principaux ont été suivis, qui sont totalement indépendants. Chacun a contribué à l'identification ou à la génération de clauses apprises pertinentes. Ces travaux peuvent être combinés afin de contribuer à la création d'un solveur spécialisé dans la résolution d'instances BMC.
Lieu : LRE, EPITA, 14-16 Rue Voltaire, 94270 Le Kremlin-Bicêtre
Rapporteurs/ Rapporteuses
| Personne | Qualité | Etablissement |
|---|---|---|
| M. Bounekkar Ahmed | Maître de Conférences (HDR) | ERIC |
| M. Vijay Ganesh | Professeur des universités | Programming Languages/Software Engineering, and Foundations of AI Group, Georgia Institute of Technology, Atlanta, USA (États-Unis) |
Composition du jury
| Personne | Qualité | Etablissement |
|---|---|---|
| M. Baarir Souheib | Maître de Conférences (HDR) | LIP6, Univ. de Nanterre |
| M. Renault Etienne | Enseignant-Chercheur du privé | Laboratoire de Recherche de l'EPITA, Sorbonne Université |
| Mme. Encrenaz Emmanuelle | Maîtresse de Conférences (HDR) | LIP6, Sorbonne Université |
| Mme. Petrucci Laure | Professeure des universités | Laboratoire d'Informatique de Paris Nord |
| M. Vijay Ganesh | Professeur des universités | Programming Languages/Software Engineering, and Foundations of AI Group, Georgia Institute of Technology, Atlanta, USA (États-Unis) |
| M. Bounekkar Ahmed | Maître de Conférences (HDR) | ERIC |