Aarhus University Seal / Aarhus Universitets segl

Special talk by Konstantinos Sagonas on The Quest for Optimality in Stateless Model Checking Algorithms and Tools

2019.08.26 | Søs Küster Markussen

Date Thu 29 Aug
Time 10:00 11:00
Location Nygard-395

Abstract:

In this talk, after a very brief overview of the various areas of my research, I will focus on algorithms, tools and applications of stateless model checking. Stateless model checking (SMC) is a a technique for testing and verification of concurrent programs, which is especially suited for finding concurrency errors (i.e., errors that arise only under some -but not all- thread schedulings). To combat combinatorial explosion, SMC tools need to be equipped with algorithms that avoid redundant exploration of thread schedulings. In this talk, we will present recent progress on algorithms for stateless model checking, focusing on algorithms for Dynamic Partial Order Reduction (DPOR), their implementation challenges, but also the benefits that they bring in enabling SMC tools to detect bugs fast and scale to programs of considerable size and complexity. Some open problems in this area and directions for future research will also be covered.

CS frontpage, Featured, Public/media