On-the-fly reachability and cycle detection for recursive state machines

Rajeev Alur, Swarat Chaudhuri, Kousha Etessami, P. Madhusudan

Research output: Contribution to journalConference article


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.

Original languageEnglish (US)
Pages (from-to)61-76
Number of pages16
JournalLecture Notes in Computer Science
StatePublished - Sep 19 2005
Event11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005 - Edinburgh, United Kingdom
Duration: Apr 4 2005Apr 8 2005


ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this