Durée
20h Th, 20h 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. Elle couvre les techniques d'exploration de l'espace des états, et leur 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 du cours porte sur la vérification déductive. On commencera par un bref rappel sur la satisfaisabilité propositionnelle. Ensuite, la satisfaisabilité modulo théories (SMT) et les techniques de combinaison de théories sont introduites. Quelques fragments décidables majeurs (logique du premier ordre sans quantificateur, arithmétique linéaire sur les entiers et les réels) sont considérés, avec leur procédure de décision appropriée pour une utilisation dans les solveurs SMT. Les méthodes de manipulation de quantificateurs dans SMT sont présentées. Enfin, une expérience pratique des techniques de vérification déductive est donnée à l'aide d'une plate-forme de vérification basée sur SMT.
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 (INFO9012-1), notions de logique (INFO9015-1).
Activités d'apprentissage prévues et méthodes d'enseignement
Utilisation de systèmes de vérification.
Mode d'enseignement (présentiel, à distance, hybride)
Cours donné exclusivement en présentiel
Lectures recommandées ou obligatoires et notes de cours
Disponibles sur la page web du cours.
Modalités d'évaluation et critères
Examen(s) en session
Toutes sessions confondues
- En présentiel
évaluation orale
Stage(s)
Remarques organisationnelles et modifications principales apportées au cours
Contacts
Enseignants:
Bernard Boigelot, Pascal Fontaine