Dans ce cours, nous présentons des méthodes de vérification automatique pour des systèmes probabilistes. Nous expliquons ainsi comment représenter formellement un système par un modèle et une spécification par un langage mathématique ou une formule et nous intéressons principalement aux modèles ayant des aspects probabilistes comme les chaînes de Markov et les processus de décision Markovien. Nous décrivons de plus des algorithmes de model-checking sur ces modèles. Nous utilisons également l'outil de vérification PRISM qui implémente ces algorithmes de vérification.