Improved Algorithm Complexities for Linear Temporal Logic Model Checking of Pushdown Systems

1. Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley, Reading (1995)

   MATH  Google Scholar 

2. Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques and Tools. Addison-Wesley, Reading (1986)

   Google Scholar 

3. 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)

   Chapter  Google Scholar 

4. Ball, T., Rajamani, S.K.: 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)

   Chapter  Google Scholar 

5. Basu, S., Kumar, K.N., Pokorny, L.R., Ramakrishnan, C.R.: Resource-constrained model checking of recursive programs. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 236–250. Springer, Heidelberg (2002)

   Chapter  Google Scholar 

6. Benedikt, M., Godefroid, P., Reps, T.W.: Model checking of unrestricted hierarchical state machines. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 652–666. Springer, Heidelberg (2001)

   Chapter  Google Scholar 

7. Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: International Conference on Concurrency Theory, pp. 135–150 (1997)

   Google Scholar 

8. Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification on infinite structures. North-Holland, Amsterdam (2000)

   Google Scholar 

9. Burkart, O., Steffen, B.: Model checking the full modal mu-calculus for infinite sequential processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 419–429. Springer, Heidelberg (1997)

   Google Scholar 

10. Cai, J., Paige, R.: Program derivation by fixed point computation. Science of Computer Programming 11(3), 197–261 (1989)

    Article  MATH  MathSciNet  Google Scholar 

11. Ceri, S., Gottlob, G., Tanca, L.: Logic programming and databases. Springer, New York (1990)

    Google Scholar 

12. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs, Workshop, London, UK, pp. 52–71. Springer, Heidelberg (1982)

    Chapter  Google Scholar 

13. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach. In: POPL 1983: Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 117–126. ACM Press, New York (1983)

    Chapter  Google Scholar 

14. Edmund, J., Clark, M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

15. 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)

    Chapter  Google Scholar 

16. 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)

    Chapter  Google Scholar 

17. Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. In: Proc. 2nd Int. Workshop on Verification of Infinite State Systems (INFINITY 1997). Electronic Notes in Theoretic Comp. Sci, vol. 9. Elsevier, Amsterdam (1997)

    Google Scholar 

18. Liu, Y.A., Stoller, S.D.: From datalog rules to efficient programs with time and space guarantees. In: Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, pp. 172–183. ACM Press, New York (2003)

    Chapter  Google Scholar 

19. Paige, R.: Real-time simulation of a set machine on a ram (1989)

    Google Scholar 

20. Paige, R., Koenig, S.: Finite differencing of computable expressions. ACM Trans. Program. Lang. Syst. 4(3), 402–454 (1982)

    Article  MATH  Google Scholar 

21. Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in cesar. In: Proceedings of the 5th Colloquium on International Symposium on Programming, London, UK, pp. 337–351. Springer, London (1982)

    Google Scholar 

22. Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Conference Record of POPL 1995: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, pp. 49–61 (1995)

    Google Scholar 

23. Sagonas, K., Swift, T., Warren, D.S.: XSB as an efficient deductive database engine. In: Snodgrass, R.T., Winslett, M. (eds.) Proceedings of the 1994 ACM SIGMOD International Conference on Management of Data SIGMOD 1994, pp. 442–453 (1994)

    Google Scholar 

24. Steffen, B.: Generating data flow analysis algorithms from modal specifications. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 115–139. Springer, Heidelberg (1991)

    Google Scholar 

25. Steffen, B., Classen, A., Klein, M., Knoop, J., Margaria, T.: The fixpoint-analysis machine. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 72–87. Springer, Heidelberg (1995)

    Google Scholar 

Download references