Différences

Ci-dessous, les différences entre deux révisions de la page.

--- formations:masters:ue:m2:mfv9 [2023/04/21 09:17] – supprimée - modification externe (Unknown date) 127.0.0.1
+++ formations:masters:ue:m2:mfv9 [2023/04/21 09:17] (Version actuelle) – ↷ Page déplacée de formations:masters:cours:m2:mfv9 à formations:masters:ue:m2:mfv9 treinen
@@ Ligne 1: / Ligne 1: @@
+~~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

Différences

Outils de la page