Model checking is an automated verification technique that is based on the exhaustive enumeration of the state space of a system's model. Despite the fact that the state space grows exponentially in the size of the model, algorithmic and symbolic techniques have been developed to apply model checking to realistic hardware and software systems.

In this talk, we will review a series of efforts to scale model checking by exploiting parallel computing on multi-core and/or distributed hardware. Achieving linear speedup is far from obvious, since it requires the development of parallel graph algorithms and symbolic algorithms. It also requires clever concurrent datastructures, since model checking is a highly memory-intensive task. Our research results have been accumulated in the LTSmin toolset, which won several competitions.

We will touch upon some of our concurrent data-structures (hashtables, task queues) and parallel algorithms (like Nested Depth First Search, Strongly Connected Components, and Binary Decision Diagrams). We will also demonstrate the speedup on a wide range of models, e.g. Timed Automata, Promela models, Petri Nets, and Process Algebras.

Finally, we will discuss new directions (like strategy synthesis for games, and parameterised verification) and potential applications (like railway safety verification, system's biology, and blockchain technology).