On-the-Fly Reachability and Cycle Detection for Recursive State Machines

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.

• Type: Conference
• Year: 2005
• Where: TACAS
• Authors: Rajeev Alur, Swarat Chaudhuri, Kousha Etessami, P. Madhusudan
• Keywords: Algorithms, On-the-fly Depth-first Traversal, Recursive Boolean Programs, Recursive State Machines, TACAS 2005