{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:06:52Z","timestamp":1725746812496},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642402128"},{"type":"electronic","value":"9783642402135"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40213-5_13","type":"book-chapter","created":{"date-parts":[[2013,8,29]],"date-time":"2013-08-29T05:26:23Z","timestamp":1377753983000},"page":"199-216","source":"Crossref","is-referenced-by-count":4,"title":["Push-Down Automata with Gap-Order Constraints"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[]},{"given":"Mohamed Faouzi","family":"Atig","sequence":"additional","affiliation":[]},{"given":"Giorgio","family":"Delzanno","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,8,30]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Stenman, J.: Dense-timed pushdown automata. In: LICS. IEEE Computer Society (2012)","DOI":"10.1109\/LICS.2012.15"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Stenman, J.: The minimal Cost reachability problem in priced timed pushdown systems. In: Dediu, A.-H., Mart\u00edn-Vide, C. (eds.) LATA 2012. LNCS, vol. 7183, pp. 58\u201369. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-28332-1_6"},{"key":"13_CR3","unstructured":"Abdulla, P.A., Delzanno, G.: On the coverability problem for constrained multiset rewriting. In: Proc. AVIS 2006, 5th Int. Workshop on on Automated Verification of Infinite-State Systems (2006)"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A.: Well (and Better) Quasi-Ordered Transition Systems. The Bulletin of Symbolic Logic 16(4), 457\u2013515 (2010)","DOI":"10.2178\/bsl\/1294171129"},{"key":"13_CR5","unstructured":"Abdulla, P.A., Atig, M.F., Cederberg, J.: Timed lossy channel systems. In: Proc. FSTTCS 2005, 32nd Conf. on Foundations of Software Technology and, Theoretical Computer Science (2012)"},{"key":"13_CR6","unstructured":"Abdulla, P.A., \u010cer\u0101ns, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems. In: Proc. LICS 1996, 11th IEEE Int. Symp. on Logic in Computer Science, pp. 313\u2013321 (1996)"},{"issue":"3","key":"13_CR7","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1016\/j.ic.2010.11.003","volume":"209","author":"P.A. Abdulla","year":"2011","unstructured":"Abdulla, P.A., Delzanno, G., Begin, L.V.: A classification of the expressive power of well-structured transition systems. Inf. Comput. 209(3), 248\u2013279 (2011)","journal-title":"Inf. Comput."},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Delzanno, G., Rezine, A.: Parameterized verification of infinite-state processes with global conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 145\u2013157. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-540-73368-3_17"},{"issue":"2","key":"13_CR9","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/s10703-008-0062-9","volume":"34","author":"P.A. Abdulla","year":"2009","unstructured":"Abdulla, P.A., Delzanno, G., Rezine, A.: Approximated parameterized verification of infinite-state processes with global conditions. Formal Methods in System Design 34(2), 126\u2013156 (2009)","journal-title":"Formal Methods in System Design"},{"key":"13_CR10","unstructured":"Abdulla, P.A., Nyl\u00e9n, A.: Better is better than well: On efficient verification of infinite-state systems. In: Proc. LICS 2000, 16th IEEE Int. Symp. on Logic in Computer Science, pp. 132\u2013140 (2000)"},{"key":"13_CR11","unstructured":"Atig, M.F., Ganty, P.: Approximating Petri net reachability along context-free traces. In: FSTTCS 2011. LIPIcs, vol. 13, pp. 152\u2013163. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135\u2013150. Springer, Heidelberg (1997)","DOI":"10.1007\/3-540-63141-0_10"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Bozzelli, L., Pinchinat, S.: Verification of gap-order constraint abstractions of counter systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 88\u2013103. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-27940-9_7"},{"key":"13_CR14","unstructured":"Cai, X., Ogawa, M.: Well-structured extensions of pushdown systems. In: RP 2012 (2012)"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"\u010cer\u0101ns, K.: Deciding properties of integral relational automata. In: Shamir, E., Abiteboul, S. (eds.) ICALP 1994. LNCS, vol. 820, pp. 35\u201346. Springer, Heidelberg (1994)","DOI":"10.1007\/3-540-58201-0_56"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Delzanno, G.: Automatic verification of parameterized cache coherence protocols. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 53\u201368. Springer, Heidelberg (2000)","DOI":"10.1007\/10722167_8"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Delzanno, G., Bultan, T.: Constraint-based verification of client-server protocols. In: Walsh, T. (ed.) CP 2001. LNCS, vol. 2239, pp. 286\u2013301. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-45578-7_20"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Delzanno, G., Esparza, J., Podelski, A.: Constraint-based analysis of broadcast protocols. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 50\u201366. Springer, Heidelberg (1999)","DOI":"10.1007\/3-540-48168-0_5"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Delzanno, G., Ganty, P.: Automatic verification of time sensitive cryptographic protocols. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 342\u2013356. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-24730-2_27"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Delzanno, G.: Constraint-based verification of parameterized cache coherence protocols. Formal Methods in System Design 23(3), 257\u2013301 (2003)","DOI":"10.1023\/A:1026276129010"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Delzanno, G., Podelski, A.: Model checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 223\u2013239. Springer, Heidelberg (1999)","DOI":"10.1007\/3-540-49059-0_16"},{"issue":"2","key":"13_CR22","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/s10009-011-0213-y","volume":"14","author":"G. Delzanno","year":"2012","unstructured":"Delzanno, G., Rezine, A.: A lightweight regular model checking approach for parameterized systems. STTT 14(2), 207\u2013222 (2012)","journal-title":"STTT"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"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\u2013247. Springer, Heidelberg (2000)","DOI":"10.1007\/10722167_20"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Esparza, J., Ku\u010dera, A., Mayr, R.: Model checking probabilistic pushdown automata. In: Proc. LICS 2004, 20th IEEE Int. Symp. on Logic in Computer Science, pp. 12\u201321 (2004)","DOI":"10.1109\/LICS.2004.1319596"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"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\u2013336. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-44585-4_30"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Etessami, K., Yannakakis, M.: Algorithmic verification of recursive probabilistic state machines. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 253\u2013270. Springer, Heidelberg (2005)","DOI":"10.1007\/978-3-540-31980-1_17"},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"Fribourg, L., Richardson, J.: Symbolic verification with gap-order constraints. In: Gallagher, J.P. (ed.) LOPSTR 1996. LNCS, vol. 1207, pp. 20\u201337. Springer, Heidelberg (1997)","DOI":"10.1007\/3-540-62718-9_2"},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"Marcone, A.: Foundations of BQO theory. Transactions of the American Mathematical Society 345(2) (1994)","DOI":"10.2307\/2154991"},{"issue":"1-2","key":"13_CR29","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1016\/j.scico.2005.02.009","volume":"58","author":"T.W. Reps","year":"2005","unstructured":"Reps, T.W., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Program. 58(1-2), 206\u2013263 (2005)","journal-title":"Sci. Comput. Program."},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"Reps, T.: Program analysis via graph reachability. Information & Software Technology 40(11\u201312), 701\u2013726 (1998)","DOI":"10.1016\/S0950-5849(98)00093-7"},{"issue":"1 &2","key":"13_CR31","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/0304-3975(93)90222-F","volume":"116","author":"P.Z. Revesz","year":"1993","unstructured":"Revesz, P.Z.: A closed-form evaluation for datalog queries with integer (gap)-order constraints. TCS 116(1 &2), 117\u2013149 (1993)","journal-title":"TCS"},{"key":"13_CR32","unstructured":"Rot, J., de Boer, F.S., Bonsangue, M.M.: Pushdown System Representation For Unbounded Object Creation. Tech. Rep. KIT-13, Karlsruhe Institute of Technology (July 2010)"},{"key":"13_CR33","unstructured":"Schwoon, S.: Model-Checking Pushdown Systems. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2002)"},{"key":"13_CR34","doi-asserted-by":"crossref","unstructured":"Verma, K.N., Seidl, H., Schwentick, T.: On the complexity of equational Horn clauses. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 337\u2013352. Springer, Heidelberg (2005)","DOI":"10.1007\/11532231_25"},{"key":"13_CR35","doi-asserted-by":"crossref","unstructured":"Yannakakis, M.: Graph-theoretic methods in database theory. In: PODS 1990, pp. 230\u2013242 (1990)","DOI":"10.1145\/298514.298576"}],"container-title":["Lecture Notes in Computer Science","Fundamentals of Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40213-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T20:24:32Z","timestamp":1558038272000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40213-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642402128","9783642402135"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40213-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}