# Automated Deduction, and opening to Distributed Algorithms

### Main lecturers

### 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).

- Distributed Models and Algorithms,
- Passively mobile network algorithms, Actively mobile network algorithms,
- Taming uncertainty,
- Labelled Graph Rewriting, Local Computation Systems,
- Proving distributed geometric algorithms.
- Term algebras, Equational reasoning, Unification,
- Rewriting, Confluence, Rewriting modulo a theory,
- Term orderings, Termination,

### Of interest

### Presentation slide

[pdf]
### Copy of slides

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

### Resources

- Coq (8.8 or 8.9)
installation: https://github.com/coq/coq/wiki
- Why not trying a lib for hyp names?
`opam install
coq-libhyps`
- Tutorial
1 [ .v
]
- 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:

- Randomised protocols and their certification: for instance internship
- Proof automation in graphs and swarms: for instance internship
- Certification of algorithms for (non-Euclidean) geometry: for instance internship