Iterative Cycle Detection via Delaying Explorers
Ankush Desai, Shaz Qadeer, Sriram K. Rajamani, Sanjit A. Seshia · 2015
Liveness specifications on finite-state concurrent programs are checked using algorithms to detect reachable cycles in the state-transition graph of the program. We present new algorithms for cycle detection based on the idea of prioritized search via a delaying explorer. We present thorough evaluation of our algorithms on a variety of reactive asynchronous programs, including device drivers, distributed protocols, and other benchmarks culled from the research literature.