Durée
30h Th, 10h Pr, 20h Proj.
Nombre de crédits
| Master : ingénieur civil en informatique, à finalité | 5 crédits | |||
| Master en sciences informatiques, à finalité | 5 crédits |
Enseignant
Coordinateur(s)
Langue(s) de l'unité d'enseignement
Langue anglaise
Organisation et évaluation
Enseignement au deuxième quadrimestre
Horaire
Unités d'enseignement prérequises et corequises
Les unités prérequises ou corequises sont présentées au sein de chaque programme
Contenus de l'unité d'enseignement
Le cours comporte deux parties. La première est consacrée à la vérification algorithmique de systèmes parallèles basée sur l'exploration de l'espace des états. Elle couvre les techniques d'exploration de l'espace des états, les optimisations possibles de cette exploration et son utilisation pour la vérification de formules de logique temporelle par ''vérification de modèle'' (model checking). Ce dernier problème est traité à l'aide des automates sur mots infinis auxquels une introduction est donnée. Les méthodes de vérification symbolique ainsi que les techniques d'analyse des systèmes à espace d'états infini sont aussi présentées.
La deuxième partie introduit la méthode des invariants et des assertions inductives. On étudie des techniques permettant de construire des invariants et des techniques permettant de les valider. On s'intéresse spécialement aux outils permettant d'automatiser en partie le processus de vérification, et au cas particulier fréquent où la majorité des variables du système à vérifier sont booléennes.
Acquis d'apprentissage (objectifs d'apprentissage) de l'unité d'enseignement
Introduire les bases théoriques et algorithmiques de la vérification des systèmes parallèles.
Savoirs et compétences prérequis
Notions de programmation parallèle; notions de logique (cours INFO0051-0).
Activités d'apprentissage prévues et méthodes d'enseignement
Utilisation de systèmes de vérification.
Mode d'enseignement (présentiel ; enseignement à distance)
Cours théorique, exercices sur la matière théorique, exercices de vérification.
Lectures recommandées ou obligatoires et notes de cours
disponibles sur internet.
Modalités d'évaluation et critères
Projet, examen oral
Stage(s)
Remarques organisationnelles
Contacts
Enseignants:
Bernard.Boigelot@uliege.be
Pascal.Gribomont@uliege.be
Adaptation des engagements pédagogiques suite à la pandémie de COVID-19 pour la session de mai-juin
Méthodes d'apprentissage mises en œuvre : enseignement à distance
Matière de l'évaluation
Méthodes d'évaluation
Pas d'évaluation cette année.
Contact
Adaptation des engagements pédagogiques suite à la pandémie de COVID-19 pour la session août-sept
Matière de l'évaluation
Méthodes d'évaluation (et plateforme utilisée)
Sans objet.