{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T04:06:01Z","timestamp":1725768361356},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642540127"},{"type":"electronic","value":"9783642540134"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54013-4_14","type":"book-chapter","created":{"date-parts":[[2014,1,3]],"date-time":"2014-01-03T01:08:09Z","timestamp":1388711289000},"page":"242-261","source":"Crossref","is-referenced-by-count":6,"title":["Safety Problems Are NP-complete for Flat Integer Programs with Octagonal Loops"],"prefix":"10.1007","author":[{"given":"Marius","family":"Bozga","sequence":"first","affiliation":[]},{"given":"Radu","family":"Iosif","sequence":"additional","affiliation":[]},{"given":"Filip","family":"Kone\u010dn\u00fd","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-642-36742-7_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Bansal","year":"2013","unstructured":"Bansal, K., Koskinen, E., Wies, T., Zufferey, D.: Structural counter abstraction. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 62\u201377. Springer, Heidelberg (2013)"},{"key":"14_CR2","unstructured":"Boigelot, B.: Symbolic Methods for Exploring Infinite State Spaces. PhD, Univ. de Li\u00e8ge (1999)"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/11817963_47","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with lists are counter automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 517\u2013531. Springer, Heidelberg (2006)"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-642-00768-2_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Bozga","year":"2009","unstructured":"Bozga, M., G\u00eerlea, C., Iosif, R.: Iterating octagons. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 337\u2013351. Springer, Heidelberg (2009)"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-02658-4_15","volume-title":"Computer Aided Verification","author":"M. Bozga","year":"2009","unstructured":"Bozga, M., Habermehl, P., Iosif, R., Kone\u010dn\u00fd, F., Vojnar, T.: Automatic verification of integer array programs. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 157\u2013172. Springer, Heidelberg (2009)"},{"key":"14_CR6","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.\u00a06174, pp. 227\u2013242. Springer, Heidelberg (2010)"},{"key":"14_CR7","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Safety problems are NP-complete for flat integer programs with octagonal loops. Tech. Rep. arXiv 1307.5321 (2013), http:\/\/arxiv.org\/abs\/1307.5321"},{"issue":"2","key":"14_CR8","doi-asserted-by":"crossref","first-page":"275","DOI":"10.3233\/FI-2009-0044","volume":"91","author":"M. Bozga","year":"2009","unstructured":"Bozga, M., Iosif, R., Lakhnech, Y.: Flat parametric counter automata. Fundamenta Informaticae\u00a091(2), 275\u2013303 (2009)","journal-title":"Fundamenta Informaticae"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-27940-9_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L. Bozzelli","year":"2012","unstructured":"Bozzelli, L., Pinchinat, S.: Verification of gap-order constraint abstractions of counter systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol.\u00a07148, pp. 88\u2013103. Springer, Heidelberg (2012)"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/BFb0028751","volume-title":"Computer Aided Verification","author":"H. Comon","year":"1998","unstructured":"Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and presburger arithmetic. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol.\u00a01427, pp. 268\u2013279. Springer, Heidelberg (1998)"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-39212-2_17","volume-title":"Automata, Languages, and Programming","author":"S. Demri","year":"2013","unstructured":"Demri, S., Dhar, A.K., Sangnier, A.: On the complexity of verifying regular properties on flat counter systems, In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol.\u00a07966, pp. 162\u2013173. Springer, Heidelberg (2013)"},{"key":"14_CR12","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.\u00a07364, pp. 179\u2013193. Springer, Heidelberg (2012)"},{"issue":"1","key":"14_CR13","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.jcss.2012.04.002","volume":"79","author":"S. Demri","year":"2013","unstructured":"Demri, S., Jurdzinski, M., Lachish, O., Lazic, R.: The covering and boundedness problems for branching vector addition systems. J. Comput. Syst. Sci.\u00a079(1), 23\u201338 (2013)","journal-title":"J. Comput. Syst. Sci."},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Gawlitza, T.M., Monniaux, D.: Invariant generation through strategy iteration in succinctly represented control flow graphs. Logical Methods in Computer Science\u00a08(3) (2012)","DOI":"10.2168\/LMCS-8(3:29)2012"},{"issue":"3","key":"14_CR15","doi-asserted-by":"publisher","first-page":"535","DOI":"10.1145\/322261.322270","volume":"28","author":"E.M. Gurari","year":"1981","unstructured":"Gurari, E.M., Ibarra, O.H.: The complexity of the equivalence problem for simple programs. J. ACM\u00a028(3), 535\u2013560 (1981)","journal-title":"J. ACM"},{"issue":"1","key":"14_CR16","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/322047.322058","volume":"25","author":"O.H. Ibarra","year":"1978","unstructured":"Ibarra, O.H.: Reversal-bounded multicounter machines and their decision problems. J. ACM\u00a025(1), 116\u2013133 (1978)","journal-title":"J. ACM"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Leroux, J.: Vector addition system reachability problem: a short self-contained proof. In: POPL, pp. 307\u2013316 (2011)","DOI":"10.1145\/1925844.1926421"},{"key":"14_CR18","unstructured":"Minsky, M.: Computation: Finite and Infinite Machines. Prentice-Hall (1967)"},{"key":"14_CR19","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(78)90036-1","volume":"6","author":"C. Rackoff","year":"1978","unstructured":"Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci.\u00a06, 223\u2013231 (1978)","journal-title":"Theor. Comput. Sci."},{"issue":"1&2","key":"14_CR20","doi-asserted-by":"publisher","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. Theor. Comput. Sci.\u00a0116(1&2), 117\u2013149 (1993)","journal-title":"Theor. Comput. Sci."},{"key":"14_CR21","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/S0024-3795(00)00013-6","volume":"307","author":"B.D. Schutter","year":"2000","unstructured":"Schutter, B.D.: On the ultimate behavior of the sequence of consecutive powers of a matrix in the max-plus algebra. Linear Algebra and its Applications\u00a0307, 103\u2013117 (2000)","journal-title":"Linear Algebra and its Applications"},{"key":"14_CR22","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/11532231_25","volume-title":"Automated Deduction \u2013 CADE-20","author":"K.N. Verma","year":"2005","unstructured":"Verma, K.N., Seidl, H., Schwentick, T.: On the complexity of equational Horn clauses. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 337\u2013352. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54013-4_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,13]],"date-time":"2020-08-13T07:05:13Z","timestamp":1597302313000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54013-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642540127","9783642540134"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54013-4_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}