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