Open Access. Powered by Scholars. Published by Universities.®

Engineering Commons

Open Access. Powered by Scholars. Published by Universities.®

CPS Theory

Computer Sciences

2005

Articles 1 - 1 of 1

Full-Text Articles in Engineering

On-The-Fly Reachability And Cycle Detection For Recursive State Machines, Rajeev Alur, Swarat Chaudhuri, Kousha Etessami, P. Madhusudan Apr 2005

On-The-Fly Reachability And Cycle Detection For Recursive State Machines, Rajeev Alur, Swarat Chaudhuri, Kousha Etessami, P. Madhusudan

Departmental Papers (CIS)

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.