{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:38:41Z","timestamp":1725748721796},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642408847"},{"type":"electronic","value":"9783642408854"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40885-4_5","type":"book-chapter","created":{"date-parts":[[2013,9,11]],"date-time":"2013-09-11T11:20:19Z","timestamp":1378898419000},"page":"56-70","source":"Crossref","is-referenced-by-count":0,"title":["Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages"],"prefix":"10.1007","author":[{"given":"Ralf","family":"Karrenberg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marek","family":"Ko\u0161ta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Sturm","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":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"key":"5_CR2","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1145\/2384616.2384625","volume-title":"Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2012","author":"A. Betts","year":"2012","unstructured":"Betts, A., Chong, N., Donaldson, A., Qadeer, S., Thomson, P.: Gpuverify: a verifier for gpu kernels. In: Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2012, pp. 113\u2013132. ACM, New York (2012)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT Solver. In: Piterman, N., Smolka, S. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 93\u2013107. Springer, Heidelberg (2013)"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Coutinho, B., Sampaio, D., Pereira, F.M.Q., Meira, W.: Divergence analysis and optimizations. In: 2011 International Conference on Parallel Architectures and Compilation Techniques (PACT), pp. 320\u2013329 (2011)","DOI":"10.1109\/PACT.2011.63"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1145\/1854273.1854318","volume-title":"Proceedings of the 19th International Conference on Parallel Architectures and Compilation Techniques, PACT 2010","author":"G.F. Diamos","year":"2010","unstructured":"Diamos, G.F., Kerr, A.R., Yalamanchili, S., Clark, N.: Ocelot: a dynamic optimization framework for bulk-synchronous applications in heterogeneous systems. In: Proceedings of the 19th International Conference on Parallel Architectures and Compilation Techniques, PACT 2010, pp. 353\u2013364. ACM, New York (2010)"},{"key":"5_CR7","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1145\/1993498.1993506","volume-title":"Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011","author":"S. Gulwani","year":"2011","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp. 62\u201373. ACM, New York (2011)"},{"key":"5_CR8","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1145\/1854273.1854302","volume-title":"PACT","author":"J. Gummaraju","year":"2010","unstructured":"Gummaraju, J., Morichetti, L., Houston, M., Sander, B., Gaster, B.R., Zheng, B.: Twin peaks: a software platform for heterogeneous computing on general-purpose and graphics processors. In: PACT, pp. 205\u2013216. ACM, New York (2010)"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Jaskelainen, P.O., de La Lama, C.S., Huerta, P., Takala, J.: OpenCL-based Design Methodology for Application-Specific Processors. In: SAMOS 2010, pp. 223\u2013230 (July 2010)","DOI":"10.1109\/ICSAMOS.2010.5642061"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Karrenberg, R., Hack, S.: Whole function vectorization. In: CGO, pp. 141\u2013150 (2011)","DOI":"10.1109\/CGO.2011.5764682"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-28652-0_1","volume-title":"Compiler Construction","author":"R. Karrenberg","year":"2012","unstructured":"Karrenberg, R., Hack, S.: Improving Performance of OpenCL on CPUs. In: O\u2019Boyle, M. (ed.) CC 2012. LNCS, vol.\u00a07210, pp. 1\u201320. Springer, Heidelberg (2012)"},{"key":"5_CR12","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1145\/2024724.2024754","volume-title":"Proceedings of the 48th Design Automation Conference, DAC 2011","author":"Y. Kim","year":"2011","unstructured":"Kim, Y., Shrivastava, A.: Cumapz: a tool to analyze memory access patterns in CUDA. In: Proceedings of the 48th Design Automation Conference, DAC 2011, pp. 128\u2013133. ACM, New York (2011)"},{"key":"5_CR13","unstructured":"Lattner, C., Adve, V.: LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In: CGO (March 2004)"},{"key":"5_CR14","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1145\/1882291.1882320","volume-title":"Proceedings of the Eighteenth ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2010","author":"G. Li","year":"2010","unstructured":"Li, G., Gopalakrishnan, G.: Scalable smt-based verification of GPU kernel functions. In: Proceedings of the Eighteenth ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2010, pp. 187\u2013196. ACM, New York (2010)"},{"key":"5_CR15","unstructured":"Lv, J., Li, G., Humphrey, A., Gopalakrishnan, G.: Performance degradation analysis of gpu kernels. In: Proceedings of the Workshop on Exploiting Concurrency Efficiently and Correctly 2011, EC2 2011 (2011)"},{"key":"5_CR16","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du Premier Congres de Mathematiciens des Pays Slaves, Warsaw, Poland, pp. 92\u2013101 (1929)"},{"issue":"2","key":"5_CR17","doi-asserted-by":"publisher","first-page":"98","DOI":"10.2307\/2266510","volume":"14","author":"J. Robinson","year":"1949","unstructured":"Robinson, J.: Definability and decision problems in arithmetic. J. Symb. Log.\u00a014(2), 98\u2013114 (1949)","journal-title":"J. Symb. Log."},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-89740-8_2","volume-title":"Languages and Compilers for Parallel Computing","author":"J.A. Stratton","year":"2008","unstructured":"Stratton, J.A., Stone, S.S., Hwu, W.-M.W.: MCUDA: An efficient implementation of CUDA kernels for multi-core CPUs. In: Amaral, J.N. (ed.) LCPC 2008. LNCS, vol.\u00a05335, pp. 16\u201330. Springer, Heidelberg (2008)"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Tripakis, S., Stergiou, C., Lublinerman, R.: Checking equivalence of spmd programs using non-interference. Technical Report UCB\/EECS-2010-11, EECS Department, University of California, Berkeley (January 2010)","DOI":"10.21236\/ADA538815"},{"issue":"5","key":"5_CR20","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1016\/S0747-7171(08)80051-X","volume":"10","author":"V. Weispfenning","year":"1990","unstructured":"Weispfenning, V.: The complexity of almost linear Diophantine problems. Journal of Symbolic Computation\u00a010(5), 395\u2013403 (1990)","journal-title":"Journal of Symbolic Computation"},{"key":"5_CR21","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/1806596.1806606","volume-title":"Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010","author":"Y. Yang","year":"2010","unstructured":"Yang, Y., Xiang, P., Kong, J., Zhou, H.: A GPGPU compiler for memory optimization and parallelism management. In: Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, pp. 86\u201397. ACM, New York (2010)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40885-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,6]],"date-time":"2022-03-06T00:52:17Z","timestamp":1646527937000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40885-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642408847","9783642408854"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40885-4_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}