The aim of this tutorial is to review recent progress on algorithms for stateless model checking that try to combat the combinatorial explosion in the number of program executions that need to be explored to test and/or verify safety properties of concurrent programs running under both strong and weak memory models.

Specifically, we will review state-of-the-art algorithms for dynamic partial order reduction (DPOR), compare their effectiveness, present the various notions of optimality and bounding techniques that have been proposed in the literature, and discuss how bounding and DPOR algorithms interact and why their combination is not trivial. Relevant tools of this area, most notably Nidhugg, will also be demonstrated. Finally, we will briefly present some case studies on which these tools have been successfully applied.