Abstract
A number of recent papers present efficient algorithms for LTL model checking for recursive programs with finite data structures. A common feature in all these works is that they consider infinitely long runs of the program without regard to the size of the program stack. Runs requiring unbounded stack are often a result of abstractions done to obtain a finite-data recursive program. In this paper, we introduce the notion of resource-constrained model checking where we distinguish between stack-diverging runs and finite-stack runs. It should be noted that finiteness of stack-like resources cannot be expressed in LTL. We develop resource-constrained model checking in terms of good cycle detection in a finite graph called R-graph, which is constructed from a given push-down system (PDS) and a Büchi automaton. We make the formulation of the model checker “executable” by encoding it directly as Horn clauses. We present a local algorithm to detect a good cycle in an R-graph. Furthermore, by describing the construction of R-graph as a logic program and evaluating it using tabled resolution, we do model checking without materializing the push-down system or the induced Rgraph. Preliminary experiments indicate that the local model checker is at least as efficient as existing model checkers for push-down systems.
This work was supported in part by NSF grants EIA-9705998, CCR-9876242, EIA-9805735, N000140110967, and IIS-0072927.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
R. Alur, K. Etessami, and M. Yannakakis. Analysis of recursive state machines. In Computer-Aided Verification (CAV 2001). Springer-Verlag, 2001.
T. Ball and S. Rajamani. Bebop: A symbolic model checker for boolean programs. In SPIN00: SPIN Workshop, volume 1885 of Lecture Notes in Computer Science, pages 113–130, 2000.
M. Benedikt, P. Godefroid, and T. Reps. Model checking unrestricted hierarchical state machines. In Twenty-Eighth Int. Colloq. on Automata, Languages, and Programming(ICALP 2001). Springer-Verlag, 2001.
A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model checking. In Concurrency Theory (CONCURR 1997), 1997.
O. Burkart and B. Steffen. Model checking the full-modal mu-calculus for infinite sequential processes. In Proceedings of ICALP’97, volume 1256 of Lecture Notes in Computer Science, pages 419–429, 1997.
W. Chen and D. S. Warren. Tabled evaluation with delaying for general logic programs. Journal of the ACM, 43(1):20–74, January 1996.
E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In D. Kozen, editor, Proceedings of the Workshop on Logic of Programs, Yorktown Heights, volume 131 of Lecture Notes in Computer Science, pages 52–71. Springer Verlag, 1981.
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM TOPLAS, 8(2), 1986.
J.-M. Couvreur. On-the-fly verification of linear temporal logic. In Proceedings of FM’99, volume 1708 of Lecture Notes in Computer Science, pages 253–271, 1999.
J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms for model checking pushdown systems. In Computer-Aided Verification (CAV 2000), pages 232–247. Springer-Verlag, 2000.
J. Esparza and S. Schwoon. A bdd-based model checker for recursive programs. In Computer-Aided Verification (CAV 2001), pages 324–336. Springer-Verlag, 2001.
A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown systems. In Second International Workshop on Verification of Infinite State Systems(INFINITY 1997), volume 9. Elsevier Science, 1997.
L.R. Pokorny and C.R. Ramakrishnan. LTL model checking using tabled logic programming. In Workshop on Tabling in Parsing and Deduction, 2000. Available from http://www.cs.sunysb.edu/~cram/papers.
J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proceedings of the International Symposium in Programming, volume 137 of Lecture Notes in Computer Science, Berlin, 1982. Springer-Verlag.
T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In Twenty-Second ACM Symposium on Principles of Programming Languages, pages 49–61, 1995.
D. A. Schmidt and B. Steffen. Program analysis as model checking of abstract interpretations. In Static Analysis Symposium, pages 351–380, 1998.
H. Tamaki and T. Sato. OLDT resolution with tabulation. In International Conference on Logic Programming, pages 84–98. MIT Press, 1986.
R. E. Tarjan. Depth first search and linear graph algorithms. SIAM Journal of Computing, 1(2):146–160, 1972.
XSB. The XSB logic programming system. Available from http://xsb.sourceforge.net.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Basu, S., Kumar, K.N., Pokorny, L.R., Ramakrishnan, C.R. (2002). Resource-Constrained Model Checking of Recursive Programs. In: Katoen, JP., Stevens, P. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2002. Lecture Notes in Computer Science, vol 2280. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46002-0_17
Download citation
DOI: https://doi.org/10.1007/3-540-46002-0_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43419-1
Online ISBN: 978-3-540-46002-2
eBook Packages: Springer Book Archive