Mémoires de Fin d’Etudes
Etablissement
Université de Boumerdès - M’hamed Bougara
Affiliation
Département d’Informatique
Auteur
BELKACEMI, Lila
Directeur de thèse
Mezghiche, Mohammed (Professeur)
Filière
Informatique:Programmation et Systéme
Diplôme
Magister
Titre
Formalisation de la logique temporelle dans le coq
Mots clés
Logique temporelle ; Axiomatique ; Coq (logiciel)
Résumé
L’objectif de ce travail est de fournir une formalisation de la syntaxe ainsi que la sémantique de la logique temporelle linéaire propositionnelle(LTLP) en utilisant le langage de spécification GALLINA de l’assistant de preuves Coq. Par la suite, nous donnerons une vérification formelle de terminaison de l’algorithme du tableau sémantique por cette logique dans l’assistant de preuve Coq
Date de soutenance
2014
Cote
004(043.2)/A54/BEL
Pagination
72 p.
Illusatration
ill.
Format
30 cm
Statut
Traitée
Tags & Categories
département
etablissement
université
affiliation
informatique
boumerdes
hamed
bougara
logique
temporelle
universitÉ
Établissement
univérsité
departement
établissement
établissement
boumerdes
universite
établissement
affiliation
belkacemi
boumerdès
d’informatique
département
directeur
etablissement
université