Computers are used in a wide range of applications, including
embedded control systems in cars and aircraft, cloud computing,
and the Internet. As we increasingly depend on the correct
operation of such systems, it becomes crucial to design them in a
way that ensures that they behave as expected. To do so, one has
to address two problem areas: on the one hand, partial failure
that is outside the control of a system designer (such as power
outages or bit-flips due to radiation), and on the other hand,
design faults (bugs). The former is classically addressed by
means of replication and fault-tolerant distributed algorithms,
while the latter is dealt with by rigorous software engineering
methods, such as model checking. In order to maximize the
reliability, one should deploy fault-tolerant distributed
algorithms that have been verified by model checking. However,
only very few distributed algorithms have been automatically
verified, because many aspects of distributed algorithms, such as
parameterization, faults, uncertain timing, etc. still pose
research challenges for model checking.

In this talk I will discuss several verification techniques that
we recently generalized and used for automatic verification of
distributed algorithms. These techniques include parametric
interval data and counter abstraction, offline partial order
reductions, and acceleration.

Based on joint work with Annu Gmeiner, Igor Konnov, Helmut Veith,
and Ulrich Schmid