formations:masters:ue:m2:mfv9 [UFR Informatique]

Cette page est en lecture seule. Vous pouvez afficher le texte source, mais ne pourrez pas le modifier. Contactez votre administrateur si vous pensez qu'il s'agit d'une erreur.

~~NOTOC~~

====== Méthodes Formelles de Vérification ======


===== Description =====

Les systèmes informatiques ont un rôle essentiel dans la vie moderne. Ils
gèrent des tâches extrêmement importantes dans tous les domaines des activités
humaines (communication, transport, santé, commerce, finance, armement, etc.),
et leur fiabilité est par conséquent primordiale. Ces systèmes sont d'une
grande complexité; ils doivent être conçus et vérifiés de manières rigoureuses
afin d'assurer un grand degré de confiance dans leurs comportements. Le but de
ce cours est d'introduire à certaines méthodes de conception et de
vérification de programmes de différents types et d'étudier les principes de
base pour leur preuve et pour leur vérification algorithmique.

===== Syllabus =====
==== Sujets centraux ====

  - Raisonnement sur les données, types abstraits
  - Définition inductive de fonctions,
  - Spécification logique, preuve de programmes fonctionnels
  - Spécification de programmes impératifs, invariants, pré/post conditions
  - Preuve de programmes impératifs, Logique de Hoare, correction partielle, terminaison
  - Spécification de systèmes réactifs, model-checking
  - Vérification symbolique de systèmes
  - Abstraction et raffinement d'abstraction guidée par les contre-exemples


===== Pré-requis =====

  - Logique (propositionnelle, premier ordre)
  - Algorithmes de parcours de graphes

Outils pour utilisateurs

Outils du site

Outils de la page