{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T15:57:27Z","timestamp":1780675047232,"version":"3.54.1"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031646256","type":"print"},{"value":"9783031646263","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-64626-3_17","type":"book-chapter","created":{"date-parts":[[2024,7,13]],"date-time":"2024-07-13T13:01:58Z","timestamp":1720875718000},"page":"287-305","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Verified Validation for\u00a0Affine Scheduling in\u00a0Polyhedral Compilation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-7978-4723","authenticated-orcid":false,"given":"Xuyang","family":"Li","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4337-6548","authenticated-orcid":false,"given":"Hongjin","family":"Liang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3972-9395","authenticated-orcid":false,"given":"Xinyu","family":"Feng","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,7,14]]},"reference":[{"key":"17_CR1","doi-asserted-by":"publisher","unstructured":"Bang, S., Nam, S., Chun, I., Jhoo, H.Y., Lee, J.: Smt-based translation validation for machine learning compiler. In: Computer Aided Verification: 34th International Conference, CAV 2022, Haifa, Israel, 7\u201310 August 2022, Proceedings, Part II, p. 386-407, Springer, Berlin (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_19","DOI":"10.1007\/978-3-031-13188-2_19"},{"key":"17_CR2","unstructured":"Bastoul, C.: Openscop: A specification and a library for data exchange in polyhedral compilation tools. Paris-Sud University, France (September, Technical Report (2011)"},{"key":"17_CR3","doi-asserted-by":"publisher","unstructured":"Bernstein, A.J.: Analysis of programs for parallel processing. IEEE Trans. Electron. Comput. 15, 757\u2013763 (1966). https:\/\/doi.org\/10.1109\/PGEC.1966.264565","DOI":"10.1109\/PGEC.1966.264565"},{"key":"17_CR4","doi-asserted-by":"publisher","unstructured":"Bondhugula, U., Hartono, A., Ramanujam, J., Sadayappan, P.: A practical automatic polyhedral parallelizer and locality optimizer. SIGPLAN Not. 43(6), 101\u2013113 (2008). https:\/\/doi.org\/10.1145\/1379022.1375595","DOI":"10.1145\/1379022.1375595"},{"key":"17_CR5","doi-asserted-by":"publisher","unstructured":"Boulm\u00e9, S., Mar\u00e9chaly, A., Monniaux, D., P\u00e9rin, M., Yu, H.: The verified polyhedron library: an overview. In: 2018 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), pp. 9\u201317, September 2018. https:\/\/doi.org\/10.1109\/SYNASC.2018.00014","DOI":"10.1109\/SYNASC.2018.00014"},{"key":"17_CR6","unstructured":"Chen, T., et al.: Tvm: an automated end-to-end optimizing compiler for deep learning. In: Proceedings of the 13th USENIX Conference on Operating Systems Design and Implementation, OSDI 2018, pp. 579\u2013594, USENIX Association, USA (2018)"},{"key":"17_CR7","doi-asserted-by":"publisher","unstructured":"Cl\u00e9ment, B., Cohen, A.: End-to-end translation validation for the halide language. Proc. ACM Program. Lang. 6(OOPSLA1) (2022). https:\/\/doi.org\/10.1145\/3527328","DOI":"10.1145\/3527328"},{"key":"17_CR8","doi-asserted-by":"publisher","unstructured":"Courant, N., Leroy, X.: Verified code generation for the polyhedral model. Proc. ACM Program. Lang. 5(POPL) (2021). https:\/\/doi.org\/10.1145\/3434321","DOI":"10.1145\/3434321"},{"key":"17_CR9","unstructured":"Cuervo Parrino, B., Narboux, J., Violard, E., Magaud, N.: Dealing with arithmetic overflows in the polyhedral model. In: Bondhugula, U., Loechner, V. (eds.) IMPACT 2012\u20132nd International Workshop on Polyhedral Compilation Techniques. Louis-Noel Pouchet, Paris, France, January 2012"},{"key":"17_CR10","doi-asserted-by":"publisher","unstructured":"Doerfert, J., Grosser, T., Hack, S.: Optimistic loop optimization. In: Proceedings of the 2017 International Symposium on Code Generation and Optimization, CGO 2017, pp. 292-304, IEEE Press (2017). https:\/\/doi.org\/10.1109\/CGO.2017.7863748","DOI":"10.1109\/CGO.2017.7863748"},{"key":"17_CR11","doi-asserted-by":"publisher","unstructured":"Feautrier, P.: Some efficient solutions to the affine scheduling problem: Part i. one-dimensional time. Int. J. Parall. Program. 21(5), 313\u2013348 (1992a). https:\/\/doi.org\/10.1007\/BF01407835","DOI":"10.1007\/BF01407835"},{"key":"17_CR12","doi-asserted-by":"publisher","unstructured":"Feautrier, P.: Some efficient solutions to the affine scheduling problem. part ii. multidimensional time. Int. J. Parall. Program. 21, 389\u2013420 (1992b). https:\/\/doi.org\/10.1007\/BF01379404","DOI":"10.1007\/BF01379404"},{"key":"17_CR13","doi-asserted-by":"publisher","unstructured":"Feautrier, P.: Bernstein\u2019s Conditions, pp. 130\u2013134. Springer US, Boston, MA (2011).https:\/\/doi.org\/10.1007\/978-0-387-09766-4_521","DOI":"10.1007\/978-0-387-09766-4_521"},{"key":"17_CR14","doi-asserted-by":"publisher","unstructured":"Feautrier, P., Lengauer, C.: Polyhedron model. In: Padua, D. (ed.) Encyclopedia of Parallel Computing, pp. 1581\u20131592, Springer, Boston (2011). https:\/\/doi.org\/10.1007\/978-0-387-09766-4_502","DOI":"10.1007\/978-0-387-09766-4_502"},{"key":"17_CR15","doi-asserted-by":"publisher","unstructured":"Gourdin, L., Bonneau, B., Boulm\u00e9, S., Monniaux, D., B\u00e9rard, A.: Formally verifying optimizations with block simulations. Proc. ACM Program. Lang. 7(OOPSLA2) (2023). https:\/\/doi.org\/10.1145\/3622799","DOI":"10.1145\/3622799"},{"key":"17_CR16","volume-title":"1st International Workshop on Polyhedral Compilation Techniques (IMPACT)","author":"T Grosser","year":"2011","unstructured":"Grosser, T., Zheng, H., Aloor, R., Simb\u00fcrger, A., Gr\u00f6\u00dflinger, A., Pouchet, L.N.: Polly - polyhedral optimization in LLVM. In: Alias, C., Bastoul, C. (eds.) 1st International Workshop on Polyhedral Compilation Techniques (IMPACT). Chamonix, France (2011)"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/978-3-642-28869-2_20","volume-title":"Programming Languages and Systems","author":"J-H Jourdan","year":"2012","unstructured":"Jourdan, J.-H., Pottier, F., Leroy, X.: Validating LR(1) parsers. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 397\u2013416. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_20"},{"key":"17_CR18","unstructured":"Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert memory model, version 2. Research report RR-7987, INRIA (Jun 2012)"},{"key":"17_CR19","doi-asserted-by":"publisher","unstructured":"Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformations. J. Autom. Reasoning 41(1), 1\u201331 (2008). https:\/\/doi.org\/10.1007\/s10817-008-9099-0","DOI":"10.1007\/s10817-008-9099-0"},{"key":"17_CR20","doi-asserted-by":"publisher","unstructured":"Liu, A., Bernstein, G.L., Chlipala, A., Ragan-Kelley, J.: Verified tensor-program optimization via high-level scheduling rewrites. Proc. ACM Program. Lang. 6(POPL) (2022). https:\/\/doi.org\/10.1145\/3498717","DOI":"10.1145\/3498717"},{"key":"17_CR21","doi-asserted-by":"publisher","unstructured":"Livinskii, V., Babokin, D., Regehr, J.: Fuzzing loop optimizations in compilers for c++ and data-parallel languages. Proc. ACM Program. Lang. 7(PLDI) (2023). https:\/\/doi.org\/10.1145\/3591295","DOI":"10.1145\/3591295"},{"key":"17_CR22","doi-asserted-by":"publisher","unstructured":"Monniaux, D., Six, C.: Formally verified loop-invariant code motion and assorted optimizations. ACM Trans. Embed. Comput. Syst. 22(1) (2022). https:\/\/doi.org\/10.1145\/3529507","DOI":"10.1145\/3529507"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-662-53413-7_19","volume-title":"Static Analysis","author":"KS Namjoshi","year":"2016","unstructured":"Namjoshi, K.S., Singhania, N.: Loopy: programmable and formally verified loop transformations. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 383\u2013402. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53413-7_19"},{"key":"17_CR24","unstructured":"Pilkiewicz, A.: s2sloop: a validator for polyhedral transformations. https:\/\/github.com\/pilki\/s2sLoop (2010-2013)"},{"key":"17_CR25","unstructured":"Pop, S., Cohen, A., Bastoul, C., Girbal, S., Silber, G.A., Vasilache, N.: Graphite: polyhedral analyses and optimizations for QCC. In: Proceedings of the 2006 GCC Developers Summit, p. 2006 (2006)"},{"key":"17_CR26","unstructured":"Pouchet, L.N., Bondhugula, U., et\u00a0al.: The polybench benchmarks. https:\/\/www.cs.colostate.edu\/~pouchet\/software\/polybench\/ (2010-2015)"},{"key":"17_CR27","doi-asserted-by":"publisher","unstructured":"Ragan-Kelley, J., et al.: Halide: decoupling algorithms from schedules for high-performance image processing. Commun. ACM 61(1), 106\u2013115 (2017). https:\/\/doi.org\/10.1145\/3150211","DOI":"10.1145\/3150211"},{"key":"17_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-642-11970-5_13","volume-title":"Compiler Construction","author":"S Rideau","year":"2010","unstructured":"Rideau, S., Leroy, X.: Validating register allocation and spilling. In: Gupta, R. (ed.) CC 2010. LNCS, vol. 6011, pp. 224\u2013243. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11970-5_13"},{"key":"17_CR29","doi-asserted-by":"publisher","unstructured":"Six, C., Gourdin, L., Boulm\u00e9, S., Monniaux, D., Fasse, J., Nardino, N.: Formally verified superblock scheduling. In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2022, pp. 40\u201354, Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3497775.3503679","DOI":"10.1145\/3497775.3503679"},{"key":"17_CR30","doi-asserted-by":"publisher","unstructured":"Tristan, J.B., Leroy, X.: Formal verification of translation validators: a case study on instruction scheduling optimizations. SIGPLAN Not. 43(1), 17\u201327 (2008). https:\/\/doi.org\/10.1145\/1328897.1328444","DOI":"10.1145\/1328897.1328444"},{"key":"17_CR31","doi-asserted-by":"publisher","unstructured":"Tristan, J.B., Leroy, X.: Verified validation of lazy code motion. SIGPLAN Not. 44(6), 316\u2013326 (2009). https:\/\/doi.org\/10.1145\/1543135.1542512","DOI":"10.1145\/1543135.1542512"},{"key":"17_CR32","doi-asserted-by":"publisher","unstructured":"Tristan, J.B., Leroy, X.: A simple, verified validator for software pipelining. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 83\u201392, Association for Computing Machinery, New York, NY, USA (2010). https:\/\/doi.org\/10.1145\/1706299.1706311","DOI":"10.1145\/1706299.1706311"},{"key":"17_CR33","unstructured":"Verdoolaege, S., Guelton, S., Grosser, T., Cohen, A.: Schedule trees. In: Rajopadhye, S., Verdoolaege, S. (eds.) Proceedings of the 4th International Workshop on Polyhedral Compilation Techniques (IMPACT), Vienna, Austria, January 2014"},{"key":"17_CR34","doi-asserted-by":"publisher","unstructured":"Zhao, J., et al.: Akg: automatic kernel generation for neural processing units using polyhedral transformations. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, pp. 1233\u20131248, Association for Computing Machinery, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3453483.3454106","DOI":"10.1145\/3453483.3454106"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-64626-3_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,12]],"date-time":"2025-03-12T16:16:53Z","timestamp":1741796213000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-64626-3_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031646256","9783031646263"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-64626-3_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"14 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Theoretical Aspects of Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Guiyang","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 August 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tase2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/tase2024.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}