{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:39:37Z","timestamp":1725748777210},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642407864"},{"type":"electronic","value":"9783642407871"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40787-1_5","type":"book-chapter","created":{"date-parts":[[2013,9,18]],"date-time":"2013-09-18T19:18:35Z","timestamp":1379531915000},"page":"76-93","source":"Crossref","is-referenced-by-count":0,"title":["Right-Universality of Visibly Pushdown Automata"],"prefix":"10.1007","author":[{"given":"V\u00e9ronique","family":"Bruy\u00e8re","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc","family":"Ducobu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Olivier","family":"Gauwin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","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":"5_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proc. STOC, pp. 202\u2013211. ACM Press (2004)","DOI":"10.1145\/1007352.1007390"},{"key":"5_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1516512.1516518","volume":"56","author":"R. Alur","year":"2009","unstructured":"Alur, R., Madhusudan, P.: Adding nesting structure to words. J. ACM\u00a056, 1\u201343 (2009)","journal-title":"J. ACM"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Bar-Yossef, Z., Fontoura, M., Josifovski, V.: Buffering in query evaluation over XML streams. In: Proc. PODS, pp. 216\u2013227. ACM Press (2005)","DOI":"10.1145\/1065167.1065195"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Benedikt, M., Jeffrey, A., Ley-Wild, R.: Stream Firewalling of XML Constraints. In: Proc. SIGMOD Conference, pp. 487\u2013498. ACM-Press (2008)","DOI":"10.1145\/1376616.1376667"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"548","DOI":"10.1007\/978-3-642-31424-7_39","volume-title":"Computer Aided Verification","author":"M. Fredrikson","year":"2012","unstructured":"Fredrikson, M., Joiner, R., Jha, S., Reps, T., Porras, P., Sa\u00efdi, H., Yegneswaran, V.: Efficient runtime policy enforcement using counterexample-guided abstraction refinement. In: Madhusudan, P., Seshia, S.A. (eds.) CIAA 2008. LNCS, vol.\u00a07358, pp. 548\u2013563. Springer, Heidelberg (2012)"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Bruy\u00e8re, V., Ducobu, M., Gauwin, O.: Visibly pushdown automata on trees: universality and u-universality, CoRR abs\/1205.2841 (2012)","DOI":"10.1007\/978-3-642-37064-9_18"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-642-37064-9_18","volume-title":"Language and Automata Theory and Applications","author":"V. Bruy\u00e8re","year":"2013","unstructured":"Bruy\u00e8re, V., Ducobu, M., Gauwin, O.: Visibly pushdown automata: Universality and inclusion via antichains. In: Dediu, A.-H., Mart\u00edn-Vide, C., Truthe, B. (eds.) LATA 2013. LNCS, vol.\u00a07810, pp. 190\u2013201. Springer, Heidelberg (2013)"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Bultan, T., Yu, F., Betin-Can, A.: Modular verification of synchronization with reentrant locks. In: Proc. MEMOCODE, pp. 59\u201368. IEEE Computer Society (2010)","DOI":"10.1109\/MEMCOD.2010.5558623"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-540-73370-6_20","volume-title":"Model Checking Software","author":"S. Chaudhuri","year":"2007","unstructured":"Chaudhuri, S., Alur, R.: Instrumenting C programs with nested word monitors. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 279\u2013283. Springer, Heidelberg (2007)"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"548","DOI":"10.1007\/978-3-642-31424-7_39","volume-title":"Computer Aided Verification","author":"M. Fredrikson","year":"2012","unstructured":"Fredrikson, M., Joiner, R., Jha, S., Reps, T., Porras, P., Sa\u00efdi, H., Yegneswaran, V.: Efficient runtime policy enforcement using counterexample-guided abstraction refinement. In: Madhusudan, P., Seshia, S.A. (eds.) Computer Aided Verification. 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012. LNCS, vol.\u00a07358, pp. 548\u2013563. Springer, Heidelberg (2012)"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11817963_5","volume-title":"Computer Aided Verification","author":"M. Wulf De","year":"2006","unstructured":"De Wulf, M., Doyen, L., Henzinger, T., Raskin, J.-F.: Antichains: A new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 17\u201330. Springer, Heidelberg (2006)"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"548","DOI":"10.1007\/978-3-642-31424-7_39","volume-title":"Computer Aided Verification","author":"M. Fredrikson","year":"2012","unstructured":"Fredrikson, M., Joiner, R., Jha, S., Reps, T., Porras, P., Sa\u00efdi, H., Yegneswaran, V.: Efficient runtime policy enforcement using counterexample-guided abstraction refinement. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 548\u2013563. Springer, Heidelberg (2012)"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-642-39212-2_22","volume-title":"Automata, Languages, and Programming","author":"O. Friedmann","year":"2013","unstructured":"Friedmann, O., Klaedtke, F., Lange, M.: Ramsey goes visibly pushdown. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol.\u00a07966, pp. 224\u2013237. Springer, Heidelberg (2013)"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-22256-6_2","volume-title":"Implementation and Application of Automata","author":"O. Gauwin","year":"2011","unstructured":"Gauwin, O., Niehren, J.: Streamable fragments of forward XPath. In: Bouchou-Markhoff, B., Caron, P., Champarnaud, J.-M., Maurel, D. (eds.) CIAA 2011. LNCS, vol.\u00a06807, pp. 3\u201315. Springer, Heidelberg (2011)"},{"key":"5_CR16","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/j.ipl.2008.08.002","volume":"109","author":"O. Gauwin","year":"2008","unstructured":"Gauwin, O., Niehren, J., Roos, Y.: Streaming tree automata. Information Processing Letters\u00a0109, 13\u201317 (2008)","journal-title":"Information Processing Letters"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-642-03409-1_12","volume-title":"Fundamentals of Computation Theory","author":"O. Gauwin","year":"2009","unstructured":"Gauwin, O., Niehren, J., Tison, S.: Earliest\u00a0query\u00a0answering for deterministic nested word automata. In: Kuty\u0142owski, M., Charatonik, W., G\u0119bala, M. (eds.) FCT 2009. LNCS, vol.\u00a05699, pp. 121\u2013132. Springer, Heidelberg (2009)"},{"key":"5_CR18","unstructured":"Glucose, \n                    \n                      www.lri.fr\/~simon\/?page=glucose"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-540-89247-2_4","volume-title":"Runtime Verification","author":"G. Ro\u015fu","year":"2008","unstructured":"Ro\u015fu, G., Chen, F., Ball, T.: Synthesizing monitors for safety properties: This time with calls and returns. In: Leucker, M. (ed.) RV 2008. LNCS, vol.\u00a05289, pp. 51\u201368. Springer, Heidelberg (2008)"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/978-3-642-28332-1_35","volume-title":"Language and Automata Theory and Applications","author":"T.V. Nguyen","year":"2012","unstructured":"Nguyen, T.V., Ohsaki, H.: On model checking for visibly pushdown automata. In: Dediu, A.-H., Mart\u00edn-Vide, C. (eds.) LATA 2012. LNCS, vol.\u00a07183, pp. 408\u2013419. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40787-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T08:01:18Z","timestamp":1558080078000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40787-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642407864","9783642407871"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40787-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}