2022-2023 / INFO0060-1

Introduction to computer systems verification

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

Bernard Boigelot, Pascal Fontaine

Coordinateur(s)

N...

Langue(s) de l'unité d'enseignement

Langue anglaise

Organisation et évaluation

Enseignement au deuxième quadrimestre

Horaire

Horaire en ligne

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

Contacts

Enseignants:
Bernard Boigelot, Pascal Fontaine


 

Association d'un ou plusieurs MOOCs