Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

2.9.2: Fondements Vérification algorithmique des programmes/ Algorithmic verification of programs (24h, 3 ECTS)

Responsable / Course manager:

Ahmed Bouajjani (IRIF, Paris 7 & CNRS)

Enseignants / Teachers 2020-21:

Ahmed Bouajjani (IRIF, Paris 7 & CNRS)

Constantin Enea (IRIF, Paris 7 & CNRS)

Horaire/Schedule 2020-21:

Lectures will be given online on Wednesdays from 08:45 to 11:45.

Evaluation 2020-21:

Subject of the exam

The solutions must be sent by e-mail until March 11th, 2pm.

The exam has two parts as specified in the subject. You are asked to send two files, one for each part. The files must be in PDF format. Please use a text editor. It is allowed to draw pictures and scan them. Please use photos only when other solutions are not available. In any case, make sure that your files are readable and of reasonable size.

Objectifs / Goals:

La vérification automatique de programmes est un domaine de recherche important et très actif. Il pose de nombreux défis scientifiques aussi bien sur le plan théorique que sur le plan pratique. Le but de ce cours est de présenter l'approche algorithmique pour la vérification de programmes, utilisant des techniques d'analyse basées sur les automates, la logique (procédures de décisions), le calcul et la représentation d'espaces (potentiellement infinis) d'accessibles, la synthèse d'invariants, l'abstraction, et des sous-approximations efficaces pour la détection de bugs. Le cours est focalisé sur les structures de données concurrentes ou distribuées, il inclus une présentation en détail des algorithmes utilisées dans les implementations de ces structures et des critères de correction relevants.

Automatic program verification is an important and active research field, which poses many theoretical and practical scientific challenges. The goal of this course is to present the algorithmic approach for program verification, using analysis techniques based on automata, logic (decision procedures), computing the set of reachable states (which is potentially infinite), invariant synthesis, abstraction, and under-approximation techniques for detecting bugs. The course focuses on concurrent or distributed data structures, it includes a thorough presentation of the algorithms used in the implementations of these data structures, and the relevant correctness criteria.

Plan / Lectures outline:

1-4. See https://www.irif.fr/~abou/cours-mpri.html

5. Introduction. Concurrent and distributed data structures. Slides Zoom recording

  • Correctness criteria: quiescent/sequential consistency, linearizability
  • Examples of concurrent data structure implementations

6. Decision procedures for checking linearizability. Slides Zoom recording

7. Reducing Linearizability to Classic Verification Problems Slides Zoom recording

8. Weak Consistency in Replicated objects. Slides Zoom recording

  • References: On Verifying Causal Consistency (the results I presented focused on one of the Causal Consistency variations presented in this paper, namely, Causal Convergence).

Stages/Internships:

Internships in the area of Program Verification are available. Please contact one of the teachers or a member of the Modeling and Verification group of IRIF.

 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA