Modern distributed services are typically built in a modular fashion using core agreement protocols, such as consensus, as building blocks. The ubiquity of this architecture has sparked valiant verification efforts in the last decade for agreement protocols as well as systems built on top of such protocols. To tackle the complexity and unboundedness of these systems, the verification efforts have primarily been based on interactive or semi-automated techniques.

In our ambitious Discover[i] project (pronounced, discovery), we seek to develop modular, scalable, and fully-automated verification approaches for distributed systems that mimic their modular design. In particular, we advocate an approach based on assuming that the underlying core protocols are verified separately, encapsulating their complexities within cleanly-defined abstractions, and reducing verification to model checking of small, finite systems.

In this tutorial, we will begin with an overview of verification strategies for modern distributed systems. We will introduce Discover[i], the modeling language Mercury, the inbuilt Mercury primitives for abstraction of agreement protocols, and a basic model checking algorithm for finite-state Mercury programs. We will then present a toolbox of reductions that can be used to enable scalable and automated reasoning for unbounded Mercury programs.

The tutorial will be examples-driven and interactive. Basic familiarity with deductive verification and model checking will be assumed.