Progress on Algorithms for Stateless Model Checking

Abstract of Invited Presentation

This invited talk will review, in a tutorial-like fashion, recent progress on algorithms for stateless model checking that try to combat the combinatorial explosion in the number of program traces that need to be explored to test and/or verify concurrent programs. Specifically, we will review state-of-the-art algorithms for dynamic partial order reduction (DPOR), compare their effectiveness, present the various bounding techniques that have been proposed, and discuss how bounding and DPOR algorithms interact and why their combination is not trivial. Time permitting, we will also present some areas on which stateless model checking has been successfully applied.