{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:28:21Z","timestamp":1767929301796,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540354284","type":"print"},{"value":"9783540354307","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11779148_1","type":"book-chapter","created":{"date-parts":[[2006,6,21]],"date-time":"2006-06-21T05:55:49Z","timestamp":1150869349000},"page":"1-13","source":"Crossref","is-referenced-by-count":53,"title":["Adding Nesting Structure to Words"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[]},{"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"1_CR1","doi-asserted-by":"publisher","first-page":"786","DOI":"10.1145\/1075382.1075387","volume":"27","author":"R. Alur","year":"2005","unstructured":"Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T., Yannakakis, M.: Analysis of recursive state machines. ACM Transactions on Programming Languages and Systems\u00a027(4), 786\u2013818 (2005)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Chaudhuri, S., Madhusudan, P.: Automata on nested trees (under submission, 2006)","DOI":"10.1007\/11817963_31"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Chaudhuri, S., Madhusudan, P.: A fixpoint calculus for local and global program flows. In: ACM POPL, pp. 153\u2013165 (2006)","DOI":"10.1145\/1111037.1111051"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-3-540-24730-2_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Alur","year":"2004","unstructured":"Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 467\u2013481. Springer, Heidelberg (2004)"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1102","DOI":"10.1007\/11523468_89","volume-title":"Automata, Languages and Programming","author":"R. Alur","year":"2005","unstructured":"Alur, R., Kumar, V., Madhusudan, P., Viswanathan, M.: Congruences for visibly pushdown languages. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 1102\u20131114. Springer, Heidelberg (2005)"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Alur, R., Madhusudan, P.: Visibly pushdown languages. In: ACM STOC, pp. 202\u2013211 (2004)","DOI":"10.1145\/1007352.1007390"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: AACM PLDI, pp. 203\u2013213 (2001)","DOI":"10.1145\/378795.378846"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/10722468_7","volume-title":"SPIN Model Checking and Software Verification","author":"T. Ball","year":"2000","unstructured":"Ball, T., Rajamani, S.: Bebop: A symbolic model checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 113\u2013130. Springer, Heidelberg (2000)"},{"issue":"5","key":"1_CR9","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1016\/0020-0190(88)90148-2","volume":"26","author":"P. Dymond","year":"1988","unstructured":"Dymond, P.: Input-driven languages are in log n depth. Inf. Process. Lett.\u00a026(5), 247\u2013250 (1988)","journal-title":"Inf. Process. Lett."},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/3-540-45657-0_45","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"2002","unstructured":"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.\u00a02404, pp. 526\u2013538. Springer, Heidelberg (2002)"},{"issue":"3","key":"1_CR11","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/S0019-9958(67)90564-5","volume":"11","author":"D.E. Knuth","year":"1967","unstructured":"Knuth, D.E.: A characterization of parenthesis languages. Information and Control\u00a011(3), 269\u2013289 (1967)","journal-title":"Information and Control"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Kumar, V., Madhusudan, P., Viswanathan, M.: Minimization, learning, and conformance testing of boolean programs (under submission, 2006)","DOI":"10.1007\/11817949_14"},{"key":"1_CR13","unstructured":"Kumar, V., Madhusudan, P., Viswanathan, M.: Visibly pushdown languages for XML. Technical Report UIUCDCS-R-2006-2704, UIUC (2006)"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/11523468_4","volume-title":"Automata, Languages and Programming","author":"L. Libkin","year":"2005","unstructured":"Libkin, L.: Logics for unranked trees: An overview. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 35\u201350. Springer, Heidelberg (2005)"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/978-3-540-30538-5_34","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"C. L\u00f6ding","year":"2004","unstructured":"L\u00f6ding, C., Madhusudan, P., Serre, O.: Visibly pushdown games. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 408\u2013420. Springer, Heidelberg (2004)"},{"issue":"3","key":"1_CR16","doi-asserted-by":"publisher","first-page":"490","DOI":"10.1145\/321406.321411","volume":"14","author":"R. McNaughton","year":"1967","unstructured":"McNaughton, R.: Parenthesis grammars. Journal of the ACM\u00a014(3), 490\u2013500 (1967)","journal-title":"Journal of the ACM"},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-45793-3_2","volume-title":"Computer Science Logic","author":"F. Neven","year":"2002","unstructured":"Neven, F.: Automata, Logic, and XML. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol.\u00a02471, pp. 2\u201326. Springer, Heidelberg (2002)"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Reps, T., Horwitz, S., Sagiv, S.: Precise interprocedural dataflow analysis via graph reachability. In: ACM POPL, pp. 49\u201361 (1995)","DOI":"10.1145\/199448.199462"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Segoufin, L., Vianu, V.: Validating streaming XML documents. In: ACM PODS, pp. 53\u201364 (2002)","DOI":"10.1145\/543613.543622"},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1007\/3-540-54233-7_154","volume-title":"Automata, Languages and Programming","author":"W. Thomas","year":"1991","unstructured":"Thomas, W.: On logics, tilings, and automata. In: Leach Albert, J., Monien, B., Rodr\u00edguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol.\u00a0510, pp. 441\u2013454. Springer, Heidelberg (1991)"},{"issue":"1","key":"1_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation\u00a0115(1), 1\u201337 (1994)","journal-title":"Information and Computation"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1007\/3-540-12689-9_92","volume-title":"Foundations of Computation Theory","author":"B. Braunm\u00fchl von","year":"1983","unstructured":"von Braunm\u00fchl, B., Verbeek, R.: Input-driven languages are recognized in log n space. In: Karpinski, M. (ed.) FCT 1983. LNCS, vol.\u00a0158, pp. 40\u201351. Springer, Heidelberg (1983)"}],"container-title":["Lecture Notes in Computer Science","Developments in Language Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11779148_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:15:43Z","timestamp":1619507743000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11779148_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540354284","9783540354307"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/11779148_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}