Techniques de vérification de modèles (Model-checking). Systèmes de transitions (à prédicats, temporisés, probabilistes). Abstractions/comparaisons des systèmes de transitions. Logiques modales (temporisées, probabilistes, floues). Vérification de modèles (explicite, temporisée, symbolique).Vérification de modèles bornée basée sur la satisfiabilité (SAT/SMT). Vérification de programmes (Software Model-checking).Vérification quantitative (probabiliste, statistique). Vérification basée sur l'approche CEGAR (CounterExample Guided Abstraction Refinement). Études de cas. Applications à divers problèmes de décision et de prédiction.