Automated Deduction, and opening to Distributed Algorithms

Main lecturers

• Xavier Urbain, Prof, Univ. Claude Bernard Lyon 1,
• Sébastien Tixeuil, Prof, Univ. Pierre et Marie Curie, Paris 6.
• Coq proof assistant: Pierre Courtieu and Lionel Rieg

Outlines

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

• Furethermore workshop
• Pactole formal model website

Presentation slide

[pdf]

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)

Resources

1. Coq (8.8 or 8.9) installation: https://github.com/coq/coq/wiki
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