Responsable / Course manager:

Ahmed Bouajjani (IRIF, Paris 7 & CNRS)

Ahmed Bouajjani (IRIF, Paris 7 & CNRS)

Constantin Enea (LIX, Ecole Polytechnique)

Lectures will be given on Fridays from 8:45 to 11:45.

The exam will take place on March 10th, 2023, 8h45, in the room 1002. The duration will be 3 hours, and you have access to course materials.

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.

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

5. Introduction. Concurrent and distributed data structures. Slides Examples of Concurrent Lists

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

6. Relationship between observational refinement and linearizability. Proving linearizability using forward simulations Slides

• References: Obs. Ref. and Lin. Proving Lin. using For. Sim.

7. Decision procedures for checking linearizability. Slides

• Complexity results
• Deciding linearizability for implementations with fixed linearization points, and fixed number of threads, respectively.
• References: Model-Checking of Correctness Conditions for Concurrent Objects On the complexity of Linearizability Verifying Concurrent Programs Against Sequential Specifications Forward Simulation Proof for Snapshots (Section 6 and Appendix D) Reducing Linearizability to State Reachability for Queues and Stacks

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.