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)


  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

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