Courses/IMC

From LRDE

Revision as of 15:10, 5 June 2014 by Daniela Becker (talk | contribs) (Created page with "{{Course |title=Introduction au Model checking |acronym=IMC |teacher=Adl |period=S5, Ing3 |audience=Majeure, CSI |optional course=non |module=Sciences Générales |prerequisit...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Titre

Introduction au Model checking

Sigle

IMC

Enseignant

Alexandre Duret-Lutz

Période

S5, Ing3

Public

Majeure, CSI"CSI" is not in the list (InfoSup, InfoSpé, Tronc-commun, Majeure, Apprentis, Cycle Ing, SCIA, AppIng, RDI, IMAGE, ...) of allowed values for the "Course audience" property.

Contrôle
Durée
Optionnel

non

Module

Sciences Générales

Prérequis

ALGO

Objectifs

Ce cours introduit la vérification formelle en générale et les techniques de model checking en particulier. L'étudiant y découvre des logiques temporelles, différents automates représentant des mots des longueur infinie, ainsi que des techniques pour manipuler ces objets.

Plan
  • Introduction de la vérification formelle et du model checking
  • Diagrammes de décision binaires (BDD)
  • Logique temporelle à temps arborescent (CTL) et vérification à l'aide de BDD
  • Diagrammes de décision hiérarchiques (SDD)
  • Logique temporelle à temps linéaire (LTL) et passage vers les automates de Büchi
  • Test de vacuité d'un automate de Büchi
  • Lutte contre l'explosion combinatoire de l'espace d'état
  • Hypothèses d'équité et automates de Streett
  • Introduction à Spin.
Documentation
Support
Journaux