This tutorial covers methods and languages for high-level executable specification of distributed algorithms and how such methods and languages help reason about and improve the algorithms. It has four parts:

(1) A quick introduction of fundamental problems and important algorithms in distributed computing, and an overview of methods and languages for expressing distributed algorithms.

This includes essential problems such as distributed consensus—from classical to blockchain—that are at the core of distributed services.

(2) High-level specification methods and languages, especially a general model, and a language DistAlgo [1], that allows both synchronous and asynchronous computations to be expressed at a high level and be directly executable.

This includes complete specifications for example algorithms.

(3) A study of how high-level specification can make the algorithms clearer, leading to easier reasoning and better understanding and, furthermore, improvements to sophisticated distributed algorithms.

This includes reasoning and specific improvements gained for example algorithms.

(4) A discussion of high-level specifications for configuring executions, simulating failures, checking safety and liveness properties, and visualization, as well as the challenges facing language design, implementation, optimization, and evolution in general.

This includes a demo and examples that participants can run on their own.

[1] Information about DistAlgo can be found at http://distalgo.cs.stonybrook.edu/tutorial.