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 2018-19:

Ahmed Bouajjani (IRIF, Paris 7 & CNRS)

Constantin Enea (IRIF, Paris 7 & CNRS)

Horaire/Schedule 2018-19:

Lectures will be on Wednesdays from 08:45 to 11:45, room 1003.

Evaluation 2018-19:

The exam is scheduled on March 6th, 8h45, Salle 1003 (pendant le créneau habituel du cours)

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. Introduction. Concurrent and distributed data structures. Slides

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

2. Decision procedures for checking linearizability. Slides

  • Complexity results
  • Deciding linearizability for implementations with fixed linearization points, and fixed number of threads, respectively.

3. Reducing Linearizability to Classic Verification Problems Slides

  • Reductions to reachability

4. Reasoning about weak memory Slides

5. Robustness against weak memories. Slides

6. Distributed data structures. Consistency Criteria. Slides

7. Distributed data structures. Verification Slides

8. Reducing Linearizability to Classic Verification Problems Slides

  • Reasoning with forward simulations

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