Iterative Cycle Detection via Delaying Explorers - Desai, Ankush; Qadeer, Shaz; Rajamani, Sriram; Seshia, Sanjit and (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.