Automated Deduction, and opening to Distributed Algorithms


Main lecturers


Outlines

This lecture describes proof automation techniques, mostly rewriting based, and their application to the verification of distributed algorithms.

Its first part studies different flavours of rewriting systems, and some of their properties. We address automated proof techniques for equational reasoning, and focus on proofs of strong normalisation (the system terminates starting from any term).

It turns out that labelled graph rewriting defines an interesting approach to distributed computing when computations are local.

The second part of the lecture is an opening on distributed computing and its mechanical/automated verification, starting with models —in particular models with mobility— and presenting approaches to formal verification in this context.

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

Presentation slide

[pdf]

Copy of slides

  1. Lecture 1 [pdf]
  2. Lecture 2 [pdf]
  3. Lecture 3 [pdf]
  4. Lecture 4 [pdf] + ex.
  5. Lecture 5:
  6. Lecture 6 [pdf]
  7. Lecture 7 [pdf]
  8. Lecture 8 [pdf]
  9. Lecture 9
    • Package TP [tgz]Matériel preuve formelle

Articles à étudier

  1. [pdf]
    Keywords: Mobile Robots, Exploration, Model-Cheking, Induction, Ring Exploration
    → Escot
  2. [pdf]
    Keywords: Mobile Robots, Gathering, Fault Tolerance, Byzantine Faults
    → Szilagyi
  3. [pdf]
    Keywords: Self-Stabilizing Systems, First Order Rewriting, Convergence
    → Noiret
  4. [pdf]
    Keywords: Termination, Term Rewriting Systems, Proof Automation, Dependency Pairs, Graphs
  5. [pdf]
    Keywords: Asynchronous system, Broadcast Abstraction, Byzantine Process, Distributed Algorithm, k-Set Agreement, Randomized Algorithm
    → Lechine
  6. [pdf]
    Keywords: Distributed Computation, Local Interaction Systems, Formal Proof
  7. [pdf]
    Keywords: Termination, Term Rewriting Systems, Proof Automation, Modularity Dependency Pairs
    → Lucas
  8. [pdf]
    Keywords: Parameterized model checking, Byzantine faults, fault- tolerant distributed algorithms, reliable broadcast
    → Duboc
  9. [pdf]
    Keywords: Asynchrony, Synchronized rounds, Reduction, state machine replication system
    → Borthelle

Internships

  1. Randomised protocols [pdf]
  2. Proof automation for distributed DB [pdf]
  3. Certification of algorithms for geometry