SPORE: Combining Symmetry and Partial Order Reduction for Model Checking

Explore a groundbreaking approach to model checking in this 20-minute conference talk from PLDI 2024. Learn about SPORE, the first stateless model checker that combines Symmetry Reduction (SR) and Partial Order Reduction (POR) in an optimal manner. Discover how SPORE leverages both program and implementation symmetries, including a novel concept of internal symmetries. Understand how this innovative technique drastically reduces the number of executions explored, significantly advancing the state-of-the-art in model checking. Gain insights into the sound and complete methodology that addresses the long-standing challenge of combining SR and POR in stateless model checking. Presented by researchers from MPI-SWS, Germany, this talk offers valuable knowledge for those interested in program verification, concurrent systems, and software testing.

[PLDI24] SPORE: Combining Symmetry and Partial Order Reduction