Konstantinos Sagonas

Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens

2022 · arXiv (Cornell University)

Stateless Model Checking (SMC) is a verification technique for concurrent programs that checks for safety violations by exploring all possible thread schedulings. It is highly effective when coupled with Dynamic Partial Order Reduction (DPOR), which …