Searching the state space of a system using enumerative and on-the-fly depth-first traversal is an established technique for model checking finite-state systems. In this paper, we propose algorithms for on-the-fly exploration of recursive state machines, or equivalently pushdown systems, which are suited for modeling the behavior of procedural programs. We present algorithms for reachability (is a bad state reachable?) as well as for fair cycle detection (is there a reachable cycle with progress?). We also report on an implementation of these algorithms to check safety and liveness properties of recursive boolean programs, and its performance on existing benchmarks. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Alur, R., Chaudhuri, S., Etessami, K., & Madhusudan, P. (2005). On-the-fly reachability and cycle detection for recursive state machines. In Lecture Notes in Computer Science (Vol. 3440, pp. 61–76). Springer Verlag. https://doi.org/10.1007/978-3-540-31980-1_5
Mendeley helps you to discover research relevant for your work.