{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T22:29:21Z","timestamp":1743114561878,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319221762"},{"type":"electronic","value":"9783319221779"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-22177-9_11","type":"book-chapter","created":{"date-parts":[[2015,8,3]],"date-time":"2015-08-03T10:05:43Z","timestamp":1438596343000},"page":"133-145","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Interprocedural Reachability for Flat Integer Programs"],"prefix":"10.1007","author":[{"given":"Pierre","family":"Ganty","sequence":"first","affiliation":[]},{"given":"Radu","family":"Iosif","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,8,4]]},"reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-40213-5_13","volume-title":"Fundamentals of Software Engineering","author":"PA Abdulla","year":"2013","unstructured":"Abdulla, P.A., Atig, M.F., Delzanno, G., Podelski, A.: Push-down automata with gap-order constraints. In: Arbab, F., Sirjani, M. (eds.) FSEN 2013. LNCS, vol. 8161, pp. 199\u2013216. Springer, Heidelberg (2013)"},{"issue":"3","key":"11_CR2","doi-asserted-by":"publisher","first-page":"16: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 56(3), 16:1\u201316:43 (2009)","journal-title":"J. ACM"},{"key":"11_CR3","unstructured":"Atig, M.F., Ganty, P.: Approximating petri net reachability along context-free traces. In: FSTTCS 2011, vol. 13. LIPIcs, pp. 152\u2013163. Schloss Dagstuhl (2011)"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-540-45069-6_12","volume-title":"Computer Aided Verification","author":"S Bardin","year":"2003","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: Fast: fast acceleration of symbolic transition systems. In: Hunt Jr, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 118\u2013121. Springer, Heidelberg (2003)"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-642-14295-6_23","volume-title":"Computer Aided Verification","author":"M Bozga","year":"2010","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Fast acceleration of ultimately periodic relations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 227\u2013242. Springer, Heidelberg (2010)"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-642-54013-4_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Bozga","year":"2014","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Safety problems are np-complete for flat integer programs with octagonal loops. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 242\u2013261. Springer, Heidelberg (2014)"},{"key":"11_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2013.12.002","volume":"523","author":"L Bozzelli","year":"2014","unstructured":"Bozzelli, L., Pinchinat, S.: Verification of gap-order constraint abstractions of counter systems. Theo. Comput. Sci. 523, 1\u201336 (2014)","journal-title":"Theo. Comput. Sci."},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-31365-3_16","volume-title":"Automated Reasoning","author":"S Demri","year":"2012","unstructured":"Demri, S., Dhar, A.K., Sangnier, A.: Taming past ltl and flat counter systems. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 179\u2013193. Springer, Heidelberg (2012)"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Esparza, J., Ganty, P.: Complexity of pattern-based verification for multithreaded programs. In: POPL 2011, pp. 499\u2013510. ACM Press (2011)","DOI":"10.1145\/1925844.1926443"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Ganty, P., Iosif, R.: Interprocedural reachability for flat integer programs. CoRR, abs\/1405.3069v3 (2015)","DOI":"10.1007\/978-3-319-22177-9_11"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-642-36742-7_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Ganty","year":"2013","unstructured":"Ganty, P., Iosif, R., Kone\u010dn\u00fd, F.: Underapproximation of procedure summaries for integer programs. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 245\u2013259. Springer, Heidelberg (2013)"},{"key":"11_CR12","volume-title":"The Mathematical Theory of Context-Free Languages","author":"S Ginsburg","year":"1966","unstructured":"Ginsburg, S.: The Mathematical Theory of Context-Free Languages. McGraw-Hill Inc., New York (1966)"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-03237-0_22","volume-title":"Static Analysis","author":"G Godoy","year":"2009","unstructured":"Godoy, G., Tiwari, A.: Invariant checking for programs with procedure calls. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 326\u2013342. Springer, Heidelberg (2009)"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-33386-6_16","volume-title":"Automated Technology for Verification and Analysis","author":"H Hojjat","year":"2012","unstructured":"Hojjat, H., Iosif, R., Kone\u010dn\u00fd, F., Kuncak, V., R\u00fcmmer, P.: Accelerating interpolants. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 187\u2013202. Springer, Heidelberg (2012)"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-642-39799-8_26","volume-title":"Computer Aided Verification","author":"D Kroening","year":"2013","unstructured":"Kroening, D., Lewis, M., Weissenbacher, G.: Under-approximating loops in c programs for fast counterexample detection. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 381\u2013396. Springer, Heidelberg (2013)"},{"key":"11_CR16","unstructured":"Lazic, R.: The reachability problem for vector addition systems with a stack is not elementary. In: RP 2012 (2012)"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Lazic, R., Schmitz, S.: Non-elementary complexities for branching VASS, MELL, and extensions. In: CSL-LICS 2014. ACM (2014)","DOI":"10.1145\/2603088.2603129"},{"issue":"1","key":"11_CR18","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1016\/S0019-9958(78)91015-X","volume":"39","author":"M Luker","year":"1978","unstructured":"Luker, M.: A family of languages having only finite-index grammars. Inf. Control 39(1), 14\u201318 (1978)","journal-title":"Inf. Control"},{"key":"11_CR19","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/BF01744305","volume":"13","author":"M Luker","year":"1980","unstructured":"Luker, M.: Control sets on grammars using depth-first derivations. Math. Syst. Theo. 13, 349\u2013359 (1980)","journal-title":"Math. Syst. Theo."},{"issue":"1","key":"11_CR20","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher-Order Symbolic Comput. 19(1), 31\u2013100 (2006)","journal-title":"Higher-Order Symbolic Comput."},{"key":"11_CR21","volume-title":"Computation: Finite and Infinite Machines","author":"M Minsky","year":"1967","unstructured":"Minsky, M.: Computation: Finite and Infinite Machines. Prentice-Hall, Upper Saddle River (1967)"},{"issue":"1","key":"11_CR22","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/0304-3975(93)90222-F","volume":"116","author":"PZ Revesz","year":"1993","unstructured":"Revesz, P.Z.: A closed-form evaluation for datalog queries with integer (gap)-order constraints. Theo. Comput. Sci. 116(1), 117\u2013149 (1993)","journal-title":"Theo. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Fundamentals of Computation Theory"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-22177-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,8]],"date-time":"2023-02-08T14:15:30Z","timestamp":1675865730000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-22177-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319221762","9783319221779"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-22177-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"4 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}