{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T23:27:02Z","timestamp":1759879622684,"version":"3.41.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2012,10,1]],"date-time":"2012-10-01T00:00:00Z","timestamp":1349049600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003130","name":"Fonds Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["G.0232.06N"],"award-info":[{"award-number":["G.0232.06N"]}],"id":[{"id":"10.13039\/501100003130","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2012,10]]},"abstract":"<jats:p>Designers often apply manual or semi-automatic loop and data transformations on array- and loop-intensive programs to improve performance. It is crucial that such transformations preserve the functionality of the program. This article presents an automatic method for constructing equivalence proofs for the class of static affine programs. The equivalence checking is performed on a dependence graph abstraction and uses a new approach based on widening to find the proper induction hypotheses for reasoning about recurrences. Unlike transitive-closure-based approaches, this widening approach can also handle nonuniform recurrences. The implementation is publicly available and is the first of its kind to fully support commutative operations.<\/jats:p>","DOI":"10.1145\/2362389.2362390","type":"journal-article","created":{"date-parts":[[2012,11,7]],"date-time":"2012-11-07T16:42:48Z","timestamp":1352306568000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":36,"title":["Equivalence checking of static affine programs using widening to handle recurrences"],"prefix":"10.1145","volume":"34","author":[{"given":"Sven","family":"Verdoolaege","sequence":"first","affiliation":[{"name":"Katholieke Universiteit Leuven, Belgium"}]},{"given":"Gerda","family":"Janssens","sequence":"additional","affiliation":[{"name":"Katholieke Universiteit Leuven, Belgium"}]},{"given":"Maurice","family":"Bruynooghe","sequence":"additional","affiliation":[{"name":"Katholieke Universiteit Leuven, Belgium"}]}],"member":"320","published-online":{"date-parts":[[2012,11,5]]},"reference":[{"volume-title":"Proceedings of the 3rd Workshop on Embedded Systems for Real-Time Multimedia (ESTImedia'05)","author":"Absar M. J.","key":"e_1_2_1_1_1","unstructured":"Absar , M. J. , Marchal , P. , and Catthoor , F . 2005. Data-Access optimization of embedded systems through selective inlining transformation . In Proceedings of the 3rd Workshop on Embedded Systems for Real-Time Multimedia (ESTImedia'05) . M. Miranda and S. Ha, Eds., IEEE Computer Society, 75--80. Absar, M. J., Marchal, P., and Catthoor, F. 2005. Data-Access optimization of embedded systems through selective inlining transformation. In Proceedings of the 3rd Workshop on Embedded Systems for Real-Time Multimedia (ESTImedia'05). M. Miranda and S. Ha, Eds., IEEE Computer Society, 75--80."},{"volume-title":"Proceedings of the International Workshop on Compilers Optimization Meets Compiler Verification. Elsevier Science, 395--409","author":"Alias C.","key":"e_1_2_1_2_1","unstructured":"Alias , C. and Barthou , D . 2003. On the recognition of algorithm templates . In Proceedings of the International Workshop on Compilers Optimization Meets Compiler Verification. Elsevier Science, 395--409 . Alias, C. and Barthou, D. 2003. On the recognition of algorithm templates. In Proceedings of the International Workshop on Compilers Optimization Meets Compiler Verification. Elsevier Science, 395--409."},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Barrett C.\n     and \n      Tinelli C\n  . \n  2007\n  . CVC3. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07). W. Damm and H. Hermanns Eds. Lecture Notes in Computer Science vol. \n  4590 Springer 298--302.   Barrett C. and Tinelli C. 2007. CVC3. In Proceedings of the 19 th International Conference on Computer Aided Verification (CAV'07). W. Damm and H. Hermanns Eds. Lecture Notes in Computer Science vol. 4590 Springer 298--302.","DOI":"10.1007\/978-3-540-73368-3_34"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1006\/jpdc.1996.1261"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/646667.700342"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1025127.1025992"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Catthoor F. Danckaert K. Kulkarni C. Brockmeyer E. Kjeldsberg P. Van Achteren T. and Omn\u00e9s T. 2002. Data Access and Storage Management for Embedded Programmable Processors. Kluwer Academic Publishers Boston MA.   Catthoor F. Danckaert K. Kulkarni C. Brockmeyer E. Kjeldsberg P. Van Achteren T. and Omn\u00e9s T. 2002. Data Access and Storage Management for Embedded Programmable Processors. Kluwer Academic Publishers Boston MA.","DOI":"10.1007\/978-1-4757-4903-8"},{"key":"e_1_2_1_8_1","unstructured":"Chen C. 2009. Omega+ library. http:\/\/ctop.cs.utah.edu\/downloads\/omega.tar.gz.  Chen C. 2009. Omega+ library. http:\/\/ctop.cs.utah.edu\/downloads\/omega.tar.gz."},{"key":"e_1_2_1_9_1","unstructured":"Cook W. Rutherford T. Scarf H. E. and Shallcross D. F. 1991. An implementation of the generalized basis reduction algorithm for integer programming. Cowles Foundation Discussion Papers 990 Cowles Foundation Yale University.  Cook W. Rutherford T. Scarf H. E. and Shallcross D. F. 1991. An implementation of the generalized basis reduction algorithm for integer programming. Cowles Foundation Discussion Papers 990 Cowles Foundation Yale University."},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming. M. Bruynooghe and M. Wirsing, Eds., Lecture Note in Computer Science","volume":"631","author":"Cousot P.","unstructured":"Cousot , P. and Cousot , R . 1992. Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation . In Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming. M. Bruynooghe and M. Wirsing, Eds., Lecture Note in Computer Science , vol. 631 , Springer, 269--295. Cousot, P. and Cousot, R. 1992. Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation. In Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming. M. Bruynooghe and M. Wirsing, Eds., Lecture Note in Computer Science, vol. 631, Springer, 269--295."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/55364.55406"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01407931"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61736-1_44"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/643470.643472"},{"volume-title":"Proceedings of the 1st Workshop on Constraints in Software Testing, Verification and Analysis. B. Blanc, A. Gotlieb, and C. Michel, Eds., 46--57","author":"Fu Q.","key":"e_1_2_1_15_1","unstructured":"Fu , Q. , Bruynooghe , M. , Janssens , G. , and Catthoor , F . 2006. Requirements for constraint solvers in verification of data-intensive embedded system software . In Proceedings of the 1st Workshop on Constraints in Software Testing, Verification and Analysis. B. Blanc, A. Gotlieb, and C. Michel, Eds., 46--57 . Fu, Q., Bruynooghe, M., Janssens, G., and Catthoor, F. 2006. Requirements for constraint solvers in verification of data-intensive embedded system software. In Proceedings of the 1st Workshop on Constraints in Software Testing, Verification and Analysis. B. Blanc, A. Gotlieb, and C. Michel, Eds., 46--57."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-008-0075-2"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629911.1630034"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/109025.109086"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Kaufmann M. Moore J. S. and Manolios P. 2000. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers Norwell MA.   Kaufmann M. Moore J. S. and Manolios P. 2000. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers Norwell MA.","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"e_1_2_1_21_1","unstructured":"Kelly W. Maslov V. Pugh W. Rosser E. Shpeisman T. and Wonnacott D. 1996a. The Omega library. Tech. rep. University of Maryland.   Kelly W. Maslov V. Pugh W. Rosser E. Shpeisman T. and Wonnacott D. 1996a. The Omega library. Tech. rep. University of Maryland."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/247013.2949463"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1543135.1542513"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.07.007"},{"volume-title":"Proceedings of ICPP. L. M. Ni and M. Valero, Eds., IEEE Computer Society, 205--213","author":"Manjunathaiah M.","key":"e_1_2_1_25_1","unstructured":"Manjunathaiah , M. , Megson , G. M. , Rajopadhye , S. V. , and Risset , T . 2001. Uniformization of affine dependance programs for parallel embedded system design . In Proceedings of ICPP. L. M. Ni and M. Valero, Eds., IEEE Computer Society, 205--213 . Manjunathaiah, M., Megson, G. M., Rajopadhye, S. V., and Risset, T. 2001. Uniformization of affine dependance programs for parallel embedded system design. In Proceedings of ICPP. L. M. Ni and M. Valero, Eds., IEEE Computer Society, 205--213."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/377792.377804"},{"volume-title":"Proceedings of the 3rd conference on IASTED International Conference. ACTA Press, 43--48","author":"Matsumoto T.","key":"e_1_2_1_27_1","unstructured":"Matsumoto , T. , Seto , K. , and Fujita , M . 2007. Formal equivalence checking for loop optimization in C programs without unrolling . In Proceedings of the 3rd conference on IASTED International Conference. ACTA Press, 43--48 . Matsumoto, T., Seto, K., and Fujita, M. 2007. Formal equivalence checking for loop optimization in C programs without unrolling. In Proceedings of the 3rd conference on IASTED International Conference. ACTA Press, 43--48."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964029"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/358438.349314"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31985-6_15"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"van Engelen R. A. and Gallivan K. A. 2001. An efficient algorithm for pointer-to-array access conversion for compiling and optimizing DSP applications. In Innovative Archs. for Future Generation High-Performance Processors and Systems. IEEE 80--89.   van Engelen R. A. and Gallivan K. A. 2001. An efficient algorithm for pointer-to-array access conversion for compiling and optimizing DSP applications. In Innovative Archs. for Future Generation High-Performance Processors and Systems. IEEE 80--89.","DOI":"10.1109\/IWIA.2001.955200"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/1888390.1888455"},{"volume-title":"Proceedings of the International Conference on Information Theory and Statistical Learning. M. Beck and T. Stoll, Eds.","author":"Verdoolaege S.","key":"e_1_2_1_34_1","unstructured":"Verdoolaege , S. and Bruynooghe , M . 2008. Algorithms for weighted counting over parametric polytopes: A survey and a practical comparison . In Proceedings of the International Conference on Information Theory and Statistical Learning. M. Beck and T. Stoll, Eds. Verdoolaege, S. and Bruynooghe, M. 2008. Algorithms for weighted counting over parametric polytopes: A survey and a practical comparison. In Proceedings of the International Conference on Information Theory and Statistical Learning. M. Beck and T. Stoll, Eds."},{"volume-title":"Proceedings of the 18th International Conference on Static Analysis. (SAS'11)","author":"Verdoolaege S.","key":"e_1_2_1_35_1","unstructured":"Verdoolaege , S. , Cohen , A. , and Beletska , A . 2011. Transitive closures of affine integer tuple relations and their overapproximations . In Proceedings of the 18th International Conference on Static Analysis. (SAS'11) . Springer, 216--232. Verdoolaege, S., Cohen, A., and Beletska, A. 2011. Transitive closures of affine integer tuple relations and their overapproximations. In Proceedings of the 18th International Conference on Static Analysis. (SAS'11). Springer, 216--232."},{"volume-title":"Proceedings of the 2nd International Workshop on Polyhedral Compilation Techniques (IMPACT'12)","author":"Verdoolaege S.","key":"e_1_2_1_36_1","unstructured":"Verdoolaege , S. and Grosser , T . 2012. Polyhedral extraction tool . In Proceedings of the 2nd International Workshop on Polyhedral Compilation Techniques (IMPACT'12) . Verdoolaege, S. and Grosser, T. 2012. Polyhedral extraction tool. In Proceedings of the 2nd International Workshop on Polyhedral Compilation Techniques (IMPACT'12)."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_44"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10836-009-5140-4"},{"key":"e_1_2_1_39_1","unstructured":"Verma M. and Marwedel P. 2007. Advanced Memory Optimization Techniques for Low-Power Embedded Processors. Springer.   Verma M. and Marwedel P. 2007. Advanced Memory Optimization Techniques for Low-Power Embedded Processors. Springer."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-3402-z"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2362389.2362390","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2362389.2362390","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:34:22Z","timestamp":1750239262000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2362389.2362390"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,10]]},"references-count":39,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,10]]}},"alternative-id":["10.1145\/2362389.2362390"],"URL":"https:\/\/doi.org\/10.1145\/2362389.2362390","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2012,10]]},"assertion":[{"value":"2010-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-11-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}