Auditorium (IMAG)
31 mai 2018 - 14h00
Raisonnement automatisé pour la Logique de Séparation avec des définitions inductives (Phd Defense)
par Cristina Serban de VERIMAG, Université Grenoble Alpes
Résumé : La contribution principale de cette thèse est un système de preuve correct et complet pour les implications entre les prédicats inductifs, fréquemment rencontrées lors de la vérification des programmes qui utilisent des structures de données récursives allouées dynamiquement. Nous introduisons un système de preuve généralisé pour la logique du premier ordre et nous l'adaptons à la logique de séparation, car ceci est un cadre qui répond aux plusieurs difficultés posées par le raisonnement sur les tas alloués dynamiquement. La correction et la complétude sont assurées par quatre restrictions sémantiques et nous proposons également un semi-algorithme de recherche de preuves qui devient une procédure de décision pour le problème d'implication lorsque les restrictions sémantiques sont respectées.
Ce raisonnement d'ordre supérieur sur les implications nécessite des procédures de décision de premier ordre pour la logique sous-jacente lors de l'application des règles d'inférence et lors de la recherche des preuves. Ainsi, nous fournissons deux procédures de décision pour la logique de séparation, en considérant le fragment sans quantificateurs et le fragment quantifié de façon Exists*Forall*, qui ont été intégrées dans le solveur SMT open source CVC4.
Finalement, nous présentons une implémentation de notre système de preuve pour la logique de séparation, qui utilise ces procédures de décision. Étant donné des prédicats inductifs et une requête d'implication, un avertissement est émis lorsqu'une ou plusieurs restrictions sémantiques sont violées. Si l'implication est valide, la sortie est une preuve. Sinon, un ou plusieurs contre-exemples sont fournis.
Jury:
- Radu Iosif - CR1, VERIMAG, Directeur de thèse
- Nikos Gorogiannis - Professeur assistant, Middlesex University London, Rapporteur
- Etienne Lozes - Professeur, Université Nice Sophia Antipolis, Rapporteur
- Wei-Ngan Chin - Professeur associé, National University of Singapore, Rapporteur
- Didier Galmiche - Professeur, Université de Lorraine, Examinateur
- Mihaela Sighireanu - Maître de Conférences, Université Paris Diderot, Examinateur
- Mnacho Echenim - Maître de Conférences, ENSIMAG/LIG, Examinateur
