{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T14:28:09Z","timestamp":1725805689448},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662452301"},{"type":"electronic","value":"9783662452318"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-45231-8_41","type":"book-chapter","created":{"date-parts":[[2014,9,26]],"date-time":"2014-09-26T15:42:39Z","timestamp":1411746159000},"page":"493-508","source":"Crossref","is-referenced-by-count":13,"title":["Verification of Polyhedral Optimizations with Constant Loop Bounds in Finite State Space Computations"],"prefix":"10.1007","author":[{"given":"Markus","family":"Schordan","sequence":"first","affiliation":[]},{"given":"Pei-Hung","family":"Lin","sequence":"additional","affiliation":[]},{"given":"Dan","family":"Quinlan","sequence":"additional","affiliation":[]},{"given":"Louis-No\u00ebl","family":"Pouchet","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"41_CR1","unstructured":"Pouchet, L.N.: PolyOpt\/C 0.2.0: A Polyhedral Compiler for ROSE (2012), \n \n http:\/\/www.cs.ucla.edu\/~pouchet\/software\/polyopt\/"},{"key":"41_CR2","unstructured":"Bondhugula, U., Hartono, A., Ramanujam, J., Sadayappan, P.: A practical automatic polyhedral program optimization system. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (June 2008)"},{"key":"41_CR3","doi-asserted-by":"crossref","unstructured":"Kong, M., Veras, R., Stock, K., Franchetti, F., Pouchet, L.N., Sadayappan, P.: When polyhedral transformations meet simd code generation. In: PLDI (June 2013)","DOI":"10.1145\/2491956.2462187"},{"key":"41_CR4","doi-asserted-by":"crossref","unstructured":"Holewinski, J., Pouchet, L.N., Sadayappan, P.: High-performance code generation for stencil computations on gpu architectures. In: ICS (June 2012)","DOI":"10.1145\/2304576.2304619"},{"key":"41_CR5","doi-asserted-by":"crossref","unstructured":"Pouchet, L.N., Zhang, P., Sadayappan, P., Cong, J.: Polyhedral-based data reuse optimization for configurable computing. In: FPGA (February 2013)","DOI":"10.1145\/2435264.2435273"},{"key":"41_CR6","unstructured":"Pouchet, L.N.: PoCC 1.2: The Polyhedral Compiler Collection (2012), \n \n http:\/\/www.cs.ucla.edu\/~pouchet\/software\/pocc\/"},{"key":"41_CR7","unstructured":"Leroy, X.: The Compcert C compiler (2014), \n \n http:\/\/compcert.inria.fr\/compcert-C.html"},{"issue":"3","key":"41_CR8","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/2362389.2362390","volume":"34","author":"S. Verdoolaege","year":"2012","unstructured":"Verdoolaege, S., Janssens, G., Bruynooghe, M.: Equivalence checking of static affine programs using widening to handle recurrences. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a034(3), 11 (2012)","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"issue":"6","key":"41_CR9","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/BF01379404","volume":"21","author":"P. Feautrier","year":"1992","unstructured":"Feautrier, P.: Some efficient solutions to the affine scheduling problem, part II: Multidimensional time. Intl. J. of Parallel Programming\u00a021(6), 389\u2013420 (1992)","journal-title":"Intl. J. of Parallel Programming"},{"key":"41_CR10","doi-asserted-by":"crossref","unstructured":"Irigoin, F., Triolet, R.: Supernode partitioning. In: ACM SIGPLAN Principles of Programming Languages, pp. 319\u2013329 (1988)","DOI":"10.1145\/73560.73588"},{"key":"41_CR11","unstructured":"Bastoul, C.: Code generation in the polyhedral model is easier than you think. In: IEEE Intl. Conf. on Parallel Architectures and Compilation Techniques (PACT 2004), Juan-les-Pins, France, pp. 7\u201316 (September 2004)"},{"key":"41_CR12","doi-asserted-by":"crossref","unstructured":"Pouchet, L.N., Bondhugula, U., Bastoul, C., Cohen, A., Ramanujam, J., Sadayappan, P., Vasilache, N.: Loop transformations: Convexity, pruning and optimization. In: POPL, pp. 549\u2013562 (January 2011)","DOI":"10.1145\/1925844.1926449"},{"issue":"3","key":"41_CR13","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10766-006-0012-3","volume":"34","author":"S. Girbal","year":"2006","unstructured":"Girbal, S., Vasilache, N., Bastoul, C., Cohen, A., Parello, D., Sigler, M., Temam, O.: Semi-automatic composition of loop transformations. Intl. J. of Parallel Programming\u00a034(3), 261\u2013317 (2006)","journal-title":"Intl. J. of Parallel Programming"},{"key":"41_CR14","unstructured":"Pouchet, L.N.: PolyBench\/C 3.2 (2012), \n \n http:\/\/www.cs.ucla.edu\/~pouchet\/software\/polybench\/"},{"key":"41_CR15","unstructured":"Allen, J., Kennedy, K.: Optimizing Compilers for Modern Architectures. Morgan Kaufmann Publishers (2002)"},{"issue":"4","key":"41_CR16","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R. Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems\u00a013(4), 451\u2013490 (1991)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"41_CR17","unstructured":"Steffen\u00a0(Organizer), B.: RERS Challenge: Rigorous Examination of Reactive Systems (2010, 2012, 2013, 2014), \n \n http:\/\/www.rers-challenge.org"},{"key":"41_CR18","unstructured":"Quinlan, D., Liao, C., Matzke, R., Schordan, M., Panas, T., Vuduc, R., Yi, Q.: ROSE Web Page (2014), \n \n http:\/\/www.rosecompiler.org"},{"issue":"11","key":"41_CR19","doi-asserted-by":"publisher","first-page":"1787","DOI":"10.1109\/TCAD.2013.2272536","volume":"32","author":"C. Karfa","year":"2013","unstructured":"Karfa, C., Banerjee, K., Sarkar, D., Mandal, C.: Verification of loop and arithmetic transformations of array-intensive behaviors. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a032(11), 1787\u20131800 (2013)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"41_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/978-3-642-14052-5_1","volume-title":"Interactive Theorem Proving","author":"G. Klein","year":"2010","unstructured":"Klein, G.: A framework for formal verification of compiler optimizations. In: Kaufmann, M., Paulson, L. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 371\u2013386. Springer, Heidelberg (2010)"},{"issue":"4","key":"41_CR21","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/1516507.1516509","volume":"31","author":"S. Kalvala","year":"2009","unstructured":"Kalvala, S., Warburton, R., Lacey, D.: Program transformations using temporal logic side conditions. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a031(4), 14 (2009)","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"41_CR22","unstructured":"Paulson, L.C.: Isabelle Page, \n \n https:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-45231-8_41","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T00:13:16Z","timestamp":1559002396000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-45231-8_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662452301","9783662452318"],"references-count":22,"URL":"http:\/\/dx.doi.org\/10.1007\/978-3-662-45231-8_41","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}
