Model Checking of Unrestricted Hierarchical State Machines

1. A. Aho, J. Hopcroft, and J. Ullman. The Design and Analysis of Computer Algorithms. Addison-Wesley, 1974.

   Google Scholar 

2. R. Alur, K. Etessami, and M. Yannakakis. Analysis of Recursive State Machines. In To appear in Proceedings of CAV 2001, Paris, July 2001.

   Google Scholar 

3. R. Alur and R. Grosu. Modular Refinement of Hierarchic State Machines. In Proceedings of the 27th ACM Symposium on Principles of Programming Languages, pages 390–402, January 2000.

   Google Scholar 

4. R. Alur, S. Kannan, and M. Yannakakis. Communicating Hierarchical State Machines. In Proceedings of the 26th International Colloquium on Automata, Languages, and Programming, volume 1644 of Lecture Notes in Computer Science, pages 169–178. Springer-Verlag, 1999.

   Chapter  Google Scholar 

5. R. Alur and M. Yannakakis. Model Checking of Hierarchical State Machines. In Proceedings of the Sixth ACM Symposium on the Foundations of Software Engineering (FSE’98), pages 175–188, 1998.

   Google Scholar 

6. A. Bouajjani, J. Esparza, and O. Maler. Reachability Analysis of Pushdown Automata: Application to Model-Checking. In Proc. of CONCUR’97, volume 1243 of Lecture Notes in Computer Science, pages 135–150. Springer-Verlag, 1997.

   Google Scholar 

7. O. Burkart and B. Steffen. Model Checking for Context-Free Processes. In Proc. of CONCUR’92, 1992.

   Google Scholar 

8. O. Burkart and B. Steffen. Model Checking the Full Modal Mu-Calculus for Infinite Sequential Processes. In Proc. of ICALP’97, volume 1256 of Lecture Notes in Computer Science, pages 419–429, Bologna, 1997. Springer-Verlag.

   Google Scholar 

9. B. Caucal and R. Monfort. On the Transition Graphs of Automata and Grammars. In Graph Theoretic Concepts in Computer Science, volume 484 of Lecture Notes in Computer Science, pages 311–337. Springer-Verlag, 1990.

   Google Scholar 

10. E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science. Elsevier/MIT Press, Amsterdam/Cambridge, 1990.

    Google Scholar 

11. E. A. Emerson and C. Lei. Efficient Model Checking in Fragments of the Propositional Mu-Calculus. In Proceedings of the First Symposium on Logic in Computer Science, pages 267–278, Cambridge, June 1986.

    Google Scholar 

12. J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient Algorithms for Model Checking Pushdown Systems. In Proceedings of the 12th Conference on Computer Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 232–247, Chicago, July 2000. Springer-Verlag.

    Chapter  Google Scholar 

13. A. Finkel, B. Willems, and P. Wolper. A Direct Symbolic Approach to Model Checking Pushdown Systems. Electronic Notes in Theoretical Comp. Sc., 9, 1997.

    Google Scholar 

14. J. Hopcroft and J. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979.

    Google Scholar 

15. S. Horwitz, T. Reps, and M. Sagiv. Demand interprocedural dataflow analysis. In Proceedings of the Third ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 104–115, New York, NY, October 1995. ACM Press.

    Chapter  Google Scholar 

16. S. Horwitz, T. Reps, M. Sagiv, and G. Rosay. Speeding up slicing. In Proceedings of the Third ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 11–20, New York, NY, December 1994. ACM Press.

    Google Scholar 

17. T. Reps. Program analysis via graph reachability. Information and Software Technology, 40(11-12):701–726, November 1998. Special issue on program slicing.

    Article  Google Scholar 

18. T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In Symp. on Princ. of Prog. Lang., pages 49–61, New York, NY, 1995. ACM Press.

    Google Scholar 

19. M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science, pages 322–331, Cambridge, June 1986.

    Google Scholar 

20. I. Walukiewicz. Pushdown Processes: Games and Model-Checking. In Proc. 8th Conference on Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 62–74, New Brunswick, August 1996. Springer-Verlag.

    Google Scholar 

21. M. Yannakakis. Graph-theoretic methods in database theory. In Proc. of the Symp. on Princ. of Database Syst., pages 230–242, 1990.

    Google Scholar 

Download references