Visibly pushdown languages. (English) Zbl 1192.68396
Proceedings of the 36th annual ACM symposium on theory of computing (STOC 2004), Chicago, IL, USA, June 13 - 15, 2004. New York, NY: ACM Press (ISBN 1-58113-852-0). 202-211, electronic only (2004).
MSC:
| 68Q42 | Grammars and rewriting systems |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q45 | Formal languages and automata |
References:
| [1] | J. Autebert, J. Berstel, L. Boasson. Context-free languages and pushdown automata. In Handbook of Formal Languages, Vol. 1, pages 111-174, Springer, 1997.]] |
| [2] | R. Alur, K. Etessami, and P. Madhusudan. A temporal logic of nested calls and returns. To appear in Proc. of Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS’04, Spain, LNCS 2988. Springer, 2004.]] · Zbl 1126.68466 |
| [3] | R. Alur, K. Etessami, and M. Yannakakis. Analysis of recursive state machines. In Proc. of the 13th International Conference on Computer Aided Verification, LNCS 2102, pages 207-220. Springer, 2001.]] · Zbl 0991.68535 |
| [4] | J. Berstel and L. Boasson. Balanced grammars and their languages. In Formal and Natural Computing: Essays Dedicated to Grzegorz Rozenberg, LNCS 2300, pages 3-25. Springer, 2002.]] · Zbl 1060.68051 |
| [5] | A. Boujjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Applications to model checking. In CONCUR’97: Concurrency Theory, Eighth International Conference, LNCS 1243, pages 135-150. Springer, 1997.]] · Zbl 1512.68135 |
| [6] | T. Ball and S. Rajamani. Bebop: A symbolic model checker for boolean programs. In SPIN 2000 Workshop on Model Checking of Software, LNCS 1885, pages 113-130. Springer, 2000.]] · Zbl 0976.68540 |
| [7] | O. Burkart and B. Steffen. Model checking for context-free processes. In CONCUR’92: Concurrency Theory, Third International Conference, LNCS 630, pages 123-137. Springer, 1992.]] |
| [8] | A. Bouquet, O. Serre and I. Walukiewicz. Pushdown games with unboundedness and regular conditions. To appear in Foundations of Software Technology and Theoretical Computer Science (FSTTCS), December 2003.]] |
| [9] | H. Comon, M. Dauchet, R. Gilleron, D. Lugiez, S. Tison and M. Tommasi. Tree automata techniques and applications. Draft, Available at http://www. grappa. univ-lille3. fr/tata/, 2002.]] |
| [10] | T. Cachat, J. Duparc and W. Thomas. Solving pushdown games with a Σ3 winning condition. In Proceedings of the 11th Annual Conference of the European Association for Computer Science Logic, CSL 2002, volume 2471 of Lecture Notes in Computer Science, pages 322-336. Springer, 2002.]] · Zbl 1020.68049 |
| [11] | R. S. Cohen and A. Y. Gold. Theory of omega-Languages. I. Characterizations of omega-Context-Free Languages. JCSS 15(2): 169-184, 1977.]] · Zbl 0363.68113 |
| [12] | K. Chatterjee, D. Ma, R. Majumdar, T. Zhao, T. A. Henzinger, and J. Palsberg. Stack size analysis for interrupt driven programs. In Proceedings of the 10th International Symposium on Static Analysis, volume LNCS 2694, pages 109-126, 2003.]] · Zbl 1067.68539 |
| [13] | H. Chen and D. Wagner. Mops: an infrastructure for examining security properties of software. In Proceedings of ACM Conference on Computer and Communications Security, pages 235-244, 2002.]] 10.1145/586110.586142 |
| [14] | J. Esparza, A. Kucera, and S. S. Schwoon. Model-checking LTL with regular valuations for pushdown systems. Information and Computation, 186(2):355-376, 2003.]] 10.1016/S0890-5401(03)00139-1 · Zbl 1078.68081 |
| [15] | T. A. Henzinger, R. Jhala, R. Majumdar, G. C. Necula, G. Sutre, and W. Weimer. Temporal-safety proofs for systems code. In CAV 02: Proc. of 14th Conf. on Computer Aided Verification, LNCS 2404, pages 526-538. Springer, 2002.]] · Zbl 1010.68507 |
| [16] | D. Harel, D. Kozen and J. Tiuryn. Dynamic Logic. MIT Press, 2000.]] · Zbl 0976.68108 |
| [17] | T. Jensen, D. Le Metayer, and T. Thorn. Verification of control flow based security properties. In Proceedings of the IEEE Symposium on Security and Privacy, pages 89-103, 1999.]] |
| [18] | D. E. Knuth. A characterization of parenthesis languages. Information and Control, 11(3):269-289, 1967.]] · Zbl 0196.01703 |
| [19] | C. Lautemann, T. Schwentick and D. Therien. Logics For context-free languages. In Proceedings of Computer Science Logic, 8th International Workshop, CSL ’94, Poland, LNCS 933, pages 205-216. Springer, 1994.]] · Zbl 1044.68631 |
| [20] | R. McNaughton. Parenthesis grammars. Journal of the ACM, 14(3):490-500, 1967.]] 10.1145/321406.321411 · Zbl 0168.01206 |
| [21] | T. Reps, S. Horwitz, and S. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In Proceedings of the ACM Symposium on Principles of Programming Languages, pages 49-61, 1995.]] 10.1145/199448.199462 |
| [22] | S. Safra. On the complexity of \(omega\)-automata. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, pages 319-327, 1988.]] |
| [23] | W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 133-191. Elsevier Science Publishers, 1990.]] · Zbl 0900.68316 |
| [24] | M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First IEEE Symposium on Logic in Computer Science, pages 332-344, 1986.]] |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
