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

  • Rajeev Alur
  • Swarat Chaudhuri
  • Kousha Etessami
  • P. Madhusudan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3440)


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.


Model Check Internal Edge Entry State Exit State Model Check Problem 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Alur, R., Etessami, K., Yannakakis, M.: Analysis of recursive state machines. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 207–220. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  2. 2.
    Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: A model checker for concurrent software. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 484–487. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  3. 3.
    Ball, T., Rajamani, S.: Bebop: A symbolic model checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 113–130. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  4. 4.
    Ball, T., Rajamani, S.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 260. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  5. 5.
    Benedikt, M., Godefroid, P., Reps, T.: Model checking of unrestricted hierarchical state machines. In: ICALP 2001. LNCS, vol. 2076, pp. 652–666 (2001)Google Scholar
  6. 6.
    Boujjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Applications to model checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243. Springer, Heidelberg (1997)Google Scholar
  7. 7.
    Burkart, O., Steffen, B.: Model checking the full modal mu-calculus for infinite sequential processes. Theoretical Computer Science 221, 251–270 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S.: Bandera: Extracting finite-state models from Java source code. In: Proc. of Intl. Conf. on Software Engg., pp. 439–448 (2000)Google Scholar
  9. 9.
    Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design 1, 275–288 (1992)CrossRefGoogle Scholar
  10. 10.
    Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: IEEE International Conference on Computer Design: VLSI in Computers and Processors, pp. 522–525 (1992)Google Scholar
  11. 11.
    Engler, D., Chelf, B., Chou, A., Hallem, S.: Checking system rules using system-specific, programmer-written compiler extensions. In: Proc. 4th USENIX OSDI, pp. 1–16 (2000)Google Scholar
  12. 12.
    Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  13. 13.
    Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 324–336. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  14. 14.
    Fähndrich, M., Foster, J.S., Su, Z., Aiken, A.: Partial online cycle elimination in inclusion constraint graphs. In: Proc. PLDI 1998, pp. 85–96 (1998)Google Scholar
  15. 15.
    Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. In: Proc. Workshop on Verification of Infinite State Systems. Electronic Notes in Theor. Comp. Sci, vol. 9. Elsevier, Amsterdam (1997)Google Scholar
  16. 16.
    Gabow, H.: Path-based depth-first search for strong and biconnected components. Inf. Process. Lett. 74(3-4), 107–114 (2000)CrossRefMathSciNetGoogle Scholar
  17. 17.
    Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G.C., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 526–538. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  18. 18.
    Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)CrossRefMathSciNetGoogle Scholar
  19. 19.
    Pearce, D.J., Kelly, P.H.J., Hankin, C.: Online cycle detection and difference propagation for pointer analysis. Software Quality Journal 12(4), 311–337 (2004)CrossRefGoogle Scholar
  20. 20.
    Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: POPL 1995, pp. 49–61 (1995)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Rajeev Alur
    • 1
  • Swarat Chaudhuri
    • 1
  • Kousha Etessami
    • 2
  • P. Madhusudan
    • 3
  1. 1.University of PennsylvaniaUSA
  2. 2.University of EdinburghUK
  3. 3.University of Illinois at Urbana-ChampaignUSA

Personalised recommendations