Iason Marmanis

• Stateless model checking (SMC) verifies a concurrent program by systematically exploring its state space. To combat the state-space explosion problem, SMC is frequently combined with Dynamic Partial Order Reduction (DPOR), a technique that avoids exploring executions that are deemed equivalent to one another. Still, DPOR’s scalability is limited by the size of the input program. This thesis improves scalability by (i) providing direct support for common coding patterns that would otherwise have to be handled inefficiently, and (ii) combining DPOR with other state-space reduction techniques. Key to our contributions is a DPOR framework that generalizes a state-of-the-art algorithm. In the first part, we extend DPOR to efficiently handle common blocking constructs such as spinloops, which typically lead to the exploration of numerous redundant executions, often exceeding the number of complete program executions. Our approach manages to eliminate the exploration of most of these blocked executions, exploring only those that indicate a liveness violation. Separately, we extend DPOR to support a class of transactional programs where many locations are accessed atomically, a scenario known to be challenging, focusing on programs with mixed-size accesses. In the second part, we explore the combination of DPOR with state- space bounding and symmetry reduction techniques to reduce the number of explored executions. Our first work on bounding combines DPOR with preemption bounding in a way that avoids exploring equivalent executions, a task that had proven to be particularly chal- lenging. Our second work on bounding resolves the remaining issues by employing a different bound definition that is better suited for DPOR. Lastly, our work on symmetry reduction leverages thread-level symmetries, as well as symmetries between equivalent operations performed by different threads, resulting in a significant reduction in the number of executions explored for programs that exhibit such symmetries.