MF-Verif: Méthodes formelles de vérification

Cours
Ahmed Bouajanni
abou@liafa.univ-paris-diderot.fr

TD
Gustavo Petri
gpetri@informatique.univ-paris-diderot.fr

Horaire
Cours: mercredi 8:30 -- 10:30
TD: jeudi 10:30 -- 12:30

Matériels

Supports de cours

Lecture 1: Abstract Data Types and Recursive Functions

Lecture 2: Logic-based Program Specification

Lecture 3: Inductive Correctness Proofs

Lecture 4: Hoare Logic

Supports des travaux dirigés

TD1: Structures des données inductives

TD2: Spécifications en logique du premier ordre

TD3: Preuve de programmes fonctionnels

TD4: Logique de Floyd-Hoare

Test: Test

TD5: Composition parallèle des modèles

TD6: LTL - Automates de Büchi

TD7: Model Checking CTL

Examen 2016