Automated Deduction, and opening to Distributed Algorithms

Main lecturers


This lecture describes distributed systems, discusses means to verify them: with proof assistants and proof automation techniques, mostly rewriting based.

Its first part studies different flavours of distributed systems, mobile robots, agents, population protocols, etc., and some of their properties, in particular resilience to Byzantine failures

The second part of the lecture adresses the mechanical/automated verification of distributed systems, starting with models —in particular models with mobility— and presenting approaches to formal verification in this context. Sessions with the Coq proof assistant are scheduled (and basically require no prerequisite).

As it turns out that labelled graph rewriting defines an interesting approach to distributed computing when computations are local, we finally address rewriting-based automated proof techniques for equational reasoning, and focus on proofs of strong normalisation (the system terminates starting from any term).

  1. Distributed Models and Algorithms,
  2. Passively mobile network algorithms, Actively mobile network algorithms,
  3. Taming uncertainty,
  4. Labelled Graph Rewriting, Local Computation Systems,
  5. Proving distributed geometric algorithms.
  6. Term algebras, Equational reasoning, Unification,
  7. Rewriting, Confluence, Rewriting modulo a theory,
  8. Term orderings, Termination,

Of interest

Presentation slide


Copy of slides

  1. Lecture 1 [pdf] (dist)
  2. Lecture 2 [pdf] (dist)
  3. Lecture 3 [pdf] (dist)
  4. Lectures 4 & 5 [pdf] (mech. proof)
  5. Lecture 6 [pdf] (mech. proof)
  6. Lecture 7 [pdf] (auto. proof)
  7. Lecture 8
  8. Lecture 9 [pdf] (auto. proof)


  1. Coq (8.8 or 8.9) installation:
  2. Why not trying a lib for hyp names? opam install coq-libhyps
  3. Tutorial 1 [ .v ]
  4. Package pactole [tgz]

Articles à étudier

  1. [pdf]
    Keywords: Synthesis, Self-Stabilization
    → Cerda
  2. [pdf]
    Keywords: Mobile Robots, Model-Cheking, Ring
  3. [pdf]
    Keywords: Certification, Self-Stabilization
    → Michelland
  4. [pdf]
    Keywords: Topology, k-Set Agreement, Consensus
    → Bondeau-Pâtissier
  5. [pdf]
    Keywords: Topology, Dynamic Epistemic Logic, Fault-tolerance
    → Giocanti
  6. [pdf]
    Keywords: Mobile Robots, Exploration, Model-Cheking, Induction, Ring Exploration
    → Chappe
  7. [pdf]
    Keywords: Mobile Robots, Gathering, Fault Tolerance, Byzantine Faults
  8. [pdf]
    Keywords: Self-Stabilizing Systems, First Order Rewriting, Convergence
    → Marcus
  9. [pdf]
    Keywords: Termination, Term Rewriting Systems, Proof Automation, Dependency Pairs, Graphs
    → Valentin
  10. [pdf]
    Keywords: Asynchronous system, Broadcast Abstraction, Byzantine Process, Distributed Algorithm, k-Set Agreement, Randomized Algorithm
    → Pouget
  11. [pdf]
    Keywords: Distributed Computation, Local Interaction Systems, Formal Proof
    → Haidar
  12. [pdf]
    Keywords: Termination, Term Rewriting Systems, Proof Automation, Modularity Dependency Pairs
    → Levy
  13. [pdf]
    Keywords: Parameterized Model-Checking, Byzantine Faults, Fault- Tolerant Distributed Algorithms, Reliable Broadcast
  14. [pdf]
    Keywords: Asynchrony, Synchronized Rounds, Reduction, State Machine Replication System

Internships 2019

Internships will take place in the context of the ANR project SAPPORO (Lyon1/Sorbonne université/CNAM/Tokyo Institute of Technology). Various subjects are available, in the following 3 main topics:
  1. Randomised protocols and their certification: for instance internship
  2. Proof automation in graphs and swarms: for instance internship
  3. Certification of algorithms for (non-Euclidean) geometry: for instance internship