Département Informatique Cnam Paris

Accueil > UES > Classements : > AISL > NFP120 : Spécification logique et validation des programmes séquentiels

NFP120 : Spécification logique et validation des programmes séquentiels

	Fiche descriptive de l'UE: Cliquez ici
	Emploi du temps de l'UE prévisionnel (sujet à modification): Cliquez ici
	Diplômes: CYC45 Diplôme d’ingénieur Cnam spé. informatique option architecture et ingénierie des systèmes et des logiciels , CYC47 Diplôme d’ingénieur Cnam spé. informatique option informatique modélisation optimisation , CYC14 Diplôme d’ingénieur Cnam spé. informatique option réseaux, systèmes et multimédia , CYC12 Diplôme d’ingénieur Cnam spé. informatique option systèmes d’information (ISI) , LG004 Licence STIG, mention informatique générale , CPN11 Titre RNCP (niveau II) concepteur en architecture informatique
	REMPLISSEZ LE FORMULAIRE D'APPRECIATION DES AUDITEURS SUR L'ENSEIGNEMENT

Responsable national : Serge Rosmorduc
Cette UE est une partie de l’UV 16472

2012-2013

Bibliographie et lexique Coq
Calcul des propositions
logique des prédicats
Sémantique
Poly de Logique de Hoare Lisez la partie 2 sur la preuve de programmes impératifs. Il s’agit d’une version plus approfondie que le cours (plutôt NFP209 que NFP120) mais dont la lecture peut aider. La partie 1 correspond à NFP119 sur la preuve de programmes fonctionnels (hors sujet pour nfp120).
TP 1 frama-c/jessie (Exercice : prouver les programmes suivants dans frama-c). Référence rapide sur jessie (en anglais) : ici.
Cours sur la vérification de bytecode
Exemples d’examens similaires utilisé en ED (anciens examens de NFP209, donc un peu plus durs que ce qui sera demandé pour NFP120). 2008 2009 2010. Toutes les corrections ne sont pas présentes pour l’instant mais pour la logique de Hoare en particulier elles y sont..

2011-2012

Proplog
Proplog, sémantique
Calcul des propositions
Datalog
Datalog, preuves
Logique des prédicats (Cours "en travaux". On a commencé les exercices de la section 5 de ce poly).
Premier TP (prolog)
Grammaires et sémantique
Grammaires et sémantique (2) ; énoncé
Hoare
Juin 2012 (corrigé)

Annales 2011

Annales

Années précédentes

Supports de cours

Feuilles d’exercices

Feuille 1

Devoirs

Devoir 1

Annales

Archives

ancien cours

Documents joints:

Cours 1 (Premiers transparents)
(PDF - 381 ko)

Cours 2 : chaînage arrière
(PDF - 146.7 ko)

Exercices sur les tableaux sémantiques
(PDF - 41.5 ko)

cours004.pdf
(PDF - 244.5 ko)

Cours 3 : proplog négatif
(PDF - 193.1 ko)

Devoir 1 2010-2011
(PDF - 81 ko)

examenSeptembre2010.pdf
(PDF - 117 ko)

corrigeexamenSeptembre2010.pdf
(PDF - 218.9 ko)

correction_nfp120_fevrier2011.pdf
(PDF - 292.9 ko)

NFP120_logique des prédicats (Une version temporaire de la partie "logique des prédicats")
(PDF - 156 ko)

NFP120_S3_ProP_SYN_008_2.pdf
(PDF - 562.9 ko)

NFP120_S2_ProPlog_008_2.pdf
(PDF - 68 ko)

NFP120_S2_ProP_008_2.pdf
(PDF - 168.8 ko)

C07_DATALOG_Preuves_008-2.pdf
(PDF - 52.5 ko)

C04_DATALOG_008-2.pdf
(PDF - 161.3 ko)

Premier TP prolog
(PDF - 69 ko)

Cours_exercices sur les DCG
(ZIP - 101.9 ko)

Second TP sur les DCG/Sémantique
(TGZ - 2 ko)

DCG/Sémantique énoncé (en travaux)
(PDF - 85.6 ko)

Annales 2011 (1)
(PDF - 139.4 ko)

Logique de Hoare
(PDF - 71.1 ko)

Corrigé de l’examen de Juin 2012
(PDF - 149.5 ko)

Logique propositionnelle (Version pdf du fichier de définition formel de la logique propositionnelle avec et sans variable.)
(PDF - 178.1 ko)

Logiques des prédicats (Extraction du fichier Coq vu en cours sur la logique des prédicats. La première version est sans quantificateur, la deuxième avec. Il n’y a pas de symboles de fonctions.)
(PDF - 719.9 ko)

Biblio et lexique Coq (Dans ce PDf vous trouverez une bibliographie permettant d’approfondir les sujets abordés dans le cours ainsi qu’un lexique pour la lecture des fichiers Coq.)
(PDF - 202.7 ko)

semantique_op.pdf
(PDF - 204.6 ko)

exercises-jessie.tgz
(TGZ - 1.7 ko)

preuveprog.book.pdf
(PDF - 405.5 ko)

ref-jessie.pdf
(PDF - 142.2 ko)

slides-2.pdf
(PDF - 760.4 ko)

fev-09-2.pdf (Annale février 2009)
(PDF - 113.7 ko)

fev-08-3.pdf
(PDF - 135.7 ko)

fev-10.pdf
(PDF - 103 ko)