Progress on Algorithms for Stateless Model Checking

Abstract of Invited Presentation

Kostis Sagonas
(Uppsala University, Sweden)

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.

Invited Presentation in John P. Gallagher, Rob van Glabbeek and Wendelin Serwe: Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation (MARS/VPT 2018), Thessaloniki, Greece, 20th April 2018, Electronic Proceedings in Theoretical Computer Science 268, pp. 6–6.
Published: 23rd March 2018. bibtex PDF

Comments and questions to:
For website issues: