{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:01:08Z","timestamp":1751662868038,"version":"3.41.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319174723"},{"type":"electronic","value":"9783319174730"}],"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-17473-0_9","type":"book-chapter","created":{"date-parts":[[2015,4,30]],"date-time":"2015-04-30T09:59:39Z","timestamp":1430387979000},"page":"131-145","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["An Approach for Proving the Correctness of Inspector\/Executor Transformations"],"prefix":"10.1007","author":[{"given":"Michael","family":"Norrish","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michelle Mills","family":"Strout","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,5,1]]},"reference":[{"issue":"1","key":"9_CR1","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1137\/0911008","volume":"11","author":"JH Saltz","year":"1990","unstructured":"Saltz, J.H.: Aggregation methods for solving sparse triangular systems on multiprocessors. SIAM J. Sci. Stat. Comput. 11(1), 123\u2013144 (1990)","journal-title":"SIAM J. Sci. Stat. Comput."},{"issue":"4","key":"9_CR2","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1109\/71.97901","volume":"2","author":"C Koelbel","year":"1991","unstructured":"Koelbel, C., Mehrotra, P.: Compiling global name-space parallel loops for distributed execution. IEEE Trans. Parallel Distrib. Syst. 2(4), 440\u2013451 (1991)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"9_CR3","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/S0065-2458(08)60707-X","volume":"45","author":"J Saltz","year":"1997","unstructured":"Saltz, J., Chang, C., Edjlali, G., Hwang, Y.S., Moon, B., Ponnusamy, R., Sharma, S., Sussman, A., Uysal, M., Agrawal, G., Das, R., Havlak, P.: Programming irregular applications: runtime support, compilation and tools. Adv. Comput. 45, 105\u2013153 (1997)","journal-title":"Adv. Comput."},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Mitchell, N., Carter, L., Ferrante, J.: Localizing non-affine array references. In: Proceedings of the International Conference on Parallel Architectures and Compilation Techniques (PACT), pp. 192\u2013202, October 1999","DOI":"10.1109\/PACT.1999.807526"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Ding, C., Kennedy, K.: Improving cache performance in dynamic applications through data and computation reorganization at run time. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 229\u2013241, May 1999","DOI":"10.1145\/301631.301670"},{"issue":"13\u201314","key":"9_CR6","doi-asserted-by":"publisher","first-page":"1861","DOI":"10.1016\/S0167-8191(00)00062-4","volume":"26","author":"H Han","year":"2000","unstructured":"Han, H., Tseng, C.W.: Efficient compiler and run-time support for parallel irregular reductions. Parallel Comput. 26(13\u201314), 1861\u20131887 (2000)","journal-title":"Parallel Comput."},{"issue":"3","key":"9_CR7","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1023\/A:1011119519789","volume":"29","author":"J Mellor-Crummey","year":"2001","unstructured":"Mellor-Crummey, J., Whalley, D., Kennedy, K.: Improving memory hierarchy performance for irregular applications using data and computation reorderings. Int. J. Parallel Prog. 29(3), 217\u2013247 (2001)","journal-title":"Int. J. Parallel Prog."},{"key":"9_CR8","first-page":"21","volume":"10","author":"CC Douglas","year":"2000","unstructured":"Douglas, C.C., Hu, J., Kowarschik, R., R\u00fcde, U., Wei\u00df, C.: Cache optimization for structured and unstructured grid multigrid. Electron. Trans. Numer. Anal. 10, 21\u201340 (2000)","journal-title":"Electron. Trans. Numer. Anal."},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/11596110_7","volume-title":"Languages and Compilers for Parallel Computing","author":"MM Strout","year":"2005","unstructured":"Strout, M.M., Carter, L., Ferrante, J., Freeman, J., Kreaseck, B.: Combining performance aspects of irregular Gauss-Seidel via sparse tiling. In: Pugh, B., Tseng, C.-W. (eds.) LCPC 2002. LNCS, vol. 2481, pp. 90\u2013110. Springer, Heidelberg (2005)"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Mohiyuddin, M., Hoemmen, M., Demmel, J., Yelick, K.: Minimizing communication in sparse matrix solvers. In: Supercomputing (2009)","DOI":"10.1145\/1654059.1654096"},{"issue":"3","key":"9_CR11","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1006\/jpdc.1994.1104","volume":"22","author":"R Das","year":"1994","unstructured":"Das, R., Uysal, M., Saltz, J., Hwang, Y.S.S.: Communication optimizations for irregular scientific computations on distributed memory architectures. J. Parallel Distrib. Comput. 22(3), 462\u2013478 (1994)","journal-title":"J. Parallel Distrib. Comput."},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28\u201332. Springer, Heidelberg (2008). http:\/\/hol.sourceforge.net"},{"key":"9_CR13","unstructured":"Saltz, J.H.: Automated problem scheduling and reduction of communication delay effects. Technical report, Yale University (1987)"},{"issue":"6","key":"9_CR14","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/BF02577866","volume":"23","author":"L Rauchwerger","year":"1995","unstructured":"Rauchwerger, L., Amato, N.M., Padua, D.A.: A scalable method for run-time loop parallelization. Int. J. Parallel Prog. 23(6), 537\u2013576 (1995)","journal-title":"Int. J. Parallel Prog."},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Zhuang, X., Eichenberger, A., Luo, Y., O\u2019Brien, K., O\u2019Brien, K.: Exploiting parallelism with dependence-aware scheduling. In: International Conference on Parallel Architectures and Compilation Techniques (PACT), pp. 193\u2013202 (2009)","DOI":"10.1109\/PACT.2009.10"},{"issue":"1","key":"9_CR16","first-page":"1:1","volume":"38","author":"TA Davis","year":"2011","unstructured":"Davis, T.A., Hu, Y.: The University of Florida sparse matrix collection. ACM Trans. Math. Softw. 38(1), 1:1\u20131:25 (2011)","journal-title":"ACM Trans. Math. Softw."},{"issue":"2","key":"9_CR17","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1109\/5.214548","volume":"81","author":"U Banerjee","year":"1993","unstructured":"Banerjee, U., Eigenmann, R., Nicolau, A., Padua, D.A.: Automatic program parallelization. Proc. IEEE 81(2), 211\u2013243 (1993)","journal-title":"Proc. IEEE"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1007\/3-540-57208-2_28","volume-title":"CONCUR 1993","author":"C Lengauer","year":"1993","unstructured":"Lengauer, C.: Loop parallelization in the polytope model. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 398\u2013416. Springer, Heidelberg (1993)"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/3-540-61736-1_44","volume-title":"The Data Parallel Programming Model","author":"P Feautrier","year":"1996","unstructured":"Feautrier, P.: Automatic parallelization in the polytope model. In: Perrin, G.-R., Darte, A. (eds.) The Data Parallel Programming Model. LNCS, vol. 1132, pp. 79\u2013103. Springer, Heidelberg (1996)"},{"key":"9_CR20","volume-title":"Optimizing Compilers for Modern Architectures: A Dependence-based Approach","author":"K Kennedy","year":"2002","unstructured":"Kennedy, K., Allen, J.R.: Optimizing Compilers for Modern Architectures: A Dependence-based Approach. Morgan Kaufmann Publishers Inc., San Francisco (2002)"},{"issue":"4","key":"9_CR21","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/BF02577771","volume":"23","author":"YQ Yang","year":"1995","unstructured":"Yang, Y.Q., Ancourt, C., Irigoin, F.: Minimal data dependence abstractions for loop transformations: extended version. Int. J. Parallel Prog. 23(4), 359\u2013388 (1995)","journal-title":"Int. J. Parallel Prog."},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Pugh, W., Wonnacott, D.: Nonlinear array dependence analysis. In: Third Workshop on Languages, Compilers, and Run-Time Systems for Scalable Computers, Troy, New York, May 1995","DOI":"10.1007\/978-1-4615-2315-4_1"},{"issue":"4","key":"9_CR23","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1023\/A:1024597010150","volume":"31","author":"S Rus","year":"2003","unstructured":"Rus, S., Hoeflinger, J., Rauchwerger, L.: Hybrid analysis: static & dynamic memory reference analysis. Int. J. Parallel Program. 31(4), 251\u2013283 (2003)","journal-title":"Int. J. Parallel Program."},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Oancea, C.E., Rauchwerger, L.: Logical inference techniques for loop parallelization. In: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2012, pp. 509\u2013520 (2012)","DOI":"10.1145\/2254064.2254124"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Strout, M.M., Carter, L., Ferrante, J.: Compile-time composition of run-time data and iteration reorderings. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, New York, June 2003","DOI":"10.1145\/781131.781142"},{"key":"9_CR26","unstructured":"Strout, M.M., LaMielle, A., Carter, L., Ferrante, J., Kreaseck, B., Olschanowsky, C.: An approach for code generation in the sparse polyhedral framework. Technical report CS-13-109, Colorado State University, December 2013"},{"key":"9_CR27","unstructured":"Kelly, W., Maslov, V., Pugh, W., Rosser, E., Shpeisman, T., Wonnacott, D.: The Omega calculator and library, version 1.1.0, November 1996"},{"key":"9_CR28","unstructured":"Strout, M.M., Carter, L., Ferrante, J.: Proof of correctness for sparse tiling of Gauss-Seidel. Technical report, UCSD Department of Computer Science and Engineering, Technical report #CS2003-0741, April 2003"},{"key":"9_CR29","first-page":"283","volume-title":"PLDI","author":"X Yang","year":"2011","unstructured":"Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: Hall, M.W., Padua, D.A. (eds.) PLDI, pp. 283\u2013294. ACM, New York (2011)"},{"issue":"7","key":"9_CR30","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"9_CR31","doi-asserted-by":"crossref","unstructured":"Arnold, G., H\u00f6lzl, J., K\u00f6ksal, A.S., Bod\u00edk, R., Sagiv, M.: Specifying and verifying sparse matrix codes. In: Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP), ICFP 2010, pp. 249\u2013260 (2010)","DOI":"10.1145\/1863543.1863581"}],"container-title":["Lecture Notes in Computer Science","Languages and Compilers for Parallel Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17473-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T18:35:35Z","timestamp":1748370935000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17473-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319174723","9783319174730"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17473-0_9","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":"1 May 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}