PLAN DE COURS AUTOMNE 2002


LOGIQUE COMPUTATIONNELLE
INF9340-10

Lundi de 15h30 à 17h, local SH-3540
Mercredi de 15h30 à 17h, local SH-3540

Professeur : Roger Villemaire
Local: PK-4630
Téléphone: (bureau) 987-3000, poste 6744
Courriel: villemaire.roger@uqam.ca
Site: http://www.info.uqam.ca/~villem

DESCRIPTION (du cours selon l'annuaire)
Déduction et calcul, déduction naturelle, logique linéaire, lambda calcul, combinateurs, catégories cartésiennes fermées, théorie des types, théorie des constructions, mécanisation des logiques d'ordre supérieur, procédures de décision, heuristiques, mathématiques constructives. Applications: programmation fonctionnelle, programmation logique, démonstration de théorèmes assistée par ordinateur, langages formels de spécifications.

CONTENU DU COURS

Introduction : Objectifs de la logique informatique. La problématique de la vérification et de la spécification de systèmes informatiques.

Modélisation de systèmes informatique : Systèmes de transitions finis. Structures de Kripke. L'outil  NuSMV. Systèmes synchrones et asynchrones. Exemples et modélisations.

Logiques temporelles : Rappels sur le calcul propositionnel. Les logiques modales et temporelles. Les logiques LTL (Linear Temporal Logic) et CTL (Computation Tree Logic). Exemples et spécifications.

Modélisation et vérification : Exemples et exercices de modélisation et vérification de propriétés à l'aide de NuSMV.

Modélisation par la logique propositionnelle : Comment les modélisations sont représentés par des formules de la logique propositionnelle. Exemple de NuSMV.

Les diagrammes de décisions binaires: Définition et construction des bdds. Usage des bdds en modélisation et vérification. Comparaison avec les tables de vérité et les forme normale disjonctive et conjonctive. Remarque sur le problème n-SAT et P=NP.

Algorithme de Davis-Putman-Logemann-Loveland : Satisfaction de formules booléennes et algorithme de Davis-Putman-Logemann-Loveland (DPLL). Application en modélisation et vérification.

Le déroulement du cours inclus des séances de laboratoire obligatoire qui auront lieu au local PK-4870. Nous nous déplaceront donc parfois vers ce local durant le cours pour utiliser des outils permettant de mettre en pratique les notions vues.

OBJECTIFS

Généraux

Ce cours vise à rendre l'étudiant apte à représenter un système informatique à l'aide d'un outil de vérification ainsi qu'à être capable de décrire des propriétés informatiques significatives à l'aide de symbolismes logiques. De plus, l'étudiant devra maîtriser les concepts théoriques sur lesquels reposent le fonctionnement des outils.

Spécifiques

Les compétences développées dans le cadre de ce cours rendront l'étudiant(e) capable:

ÉVALUATION
      Le travail de session sera un travail de modélisation, de programmation ou de recherche, dont le sujet devra être approuvé par le professeur. L'étudiant devra présenter un exposé de 45 minutes dans les dernières semaines de la session sur son sujet de travail en plus de remettre un document écrit.
 

CALENDRIER

Le calendrier suivra le contenu du cours

RÉFÉRENCES ainsi que des articles de recherche qui seront mentionné durant le cours.

SITE WEB
LOGICIEL