Portail nationalFormationRechercher par discipline

Spécification logique et validation des programmes séquentiels

Code UE : NFP120

  • Cours
  • 6 crédits
  • Volume horaire de référence
    (+ ou - 10%) : 50 heures

Responsable(s)

Pierre COURTIEU

Public, conditions d’accès et prérequis

Le cours présente progressivement toutes les connaissances requises, néanmoins il est souhaitable d'avoir des notions de logique (propositionnelle, des prédicats). L'UE NFP108 est par exemple une très bonne introduction.

Objectifs pédagogiques

Donner les principes fondamentaux d'une programmation et d'une documentation rigoureuse.
Montrer comment la documentation formelle permet la validation des logiciels.
Remarque: Ce cours comportait précédemment une longue introduction à Prolog, cet aspect du cours a été retiré.

Compétences visées

Maitrise de techniques formelles de spécification et de validation de programmes.

Mots-clés

Contenu

Programmation et logique
 
  • sémantique des formules logique
  • méthode de déduction logique: tableaux sémantiques
  • sémantique des programmes
  • méthode de déduction sur les programme: preuves de Hoare, invariants de boucles
  • Application aux programmes Java ou C (assertions, outils de validation)

Modalité d'évaluation

Une évaluation en contrôle continu est conseillée (TP, QCMs...). Un examen final sur table est obligatoire, avec un coefficient minimal de 50% de la note finale.

Cette UE apparaît dans les diplômes et certificats suivants

Chargement du résultat...
Patientez
Intitulé de la formation
Type
Modalité(s)
Lieu(x)
Intitulé de la formation Architecte en cybersécurité
Type Diplôme d'établissement
Lieu(x) À la carte
Lieu(x) Bretagne, Pays de la Loire, Provence-Alpes-Côte d'Azur
Entrée Sans niveau spécifique
Intitulé de la formation Chef de projet maîtrise d’œuvre informatique
Type Diplôme d'établissement
Lieu(x) À la carte
Lieu(x) Bretagne, Pays de la Loire
Entrée Sans niveau spécifique
Intitulé de la formation Architecte infrastructure Réseaux et Systèmes
Type Diplôme d'établissement
Lieu(x) À la carte
Lieu(x) Bretagne, Ile-de-France (sans Paris), Pays de la Loire, Provence-Alpes-Côte d'Azur
Entrée Sans niveau spécifique
Intitulé de la formation Licence informatique
Type Diplôme national (DEUST, licence, master, doctorat, diplôme d'Etat)
Lieu(x) À la carte
Lieu(x) Auvergne - Rhône-Alpes, Bourgogne - Franche-Comté, Bretagne, Centre - Val de Loire, Grand-Est, Ile-de-France (sans Paris), Liban, Nouvelle-Aquitaine, Occitanie, Paris, Pays de la Loire, Polynésie Française, Provence-Alpes-Côte d'Azur
Entrée Niveau 4 (Bac)
Intitulé de la formation Licence informatique
Type Diplôme national (DEUST, licence, master, doctorat, diplôme d'Etat)
Lieu(x) Alternance
Lieu(x) Auvergne - Rhône-Alpes, Bourgogne - Franche-Comté, Centre - Val de Loire, Hauts-de-France, Ile-de-France (sans Paris), Martinique, Normandie, Nouvelle-Aquitaine, Occitanie, Pays de la Loire, Polynésie Française, Provence-Alpes-Côte d'Azur
Entrée Niveau 4 (Bac)
Intitulé de la formation Licence informatique
Type Diplôme national (DEUST, licence, master, doctorat, diplôme d'Etat)
Lieu(x) Package
Lieu(x) Martinique
Entrée Niveau 4 (Bac)
Intitulé de la formation Type Modalité(s) Lieu(x)

Contact

EPN05 - Informatique
2 rue Conté 33.1.13A
75003 Paris
Tel :01 40 27 26 81
Safia Sider
Voir le site

Voir le calendrier, le tarif, les conditions d'accessibilité et les modalités d'inscription dans le(s) centre(s) d'enseignement qui propose(nt) cette formation.

Enseignement non encore programmé