用于验证数组密集型源代码代数变换的功能等价性检查
计算机科学中的逻辑
2011-11-09 v1
摘要
开发高能效和高性能的嵌入式软件越来越依赖于对源代码关键部分应用复杂的变换。应用此类非平凡源代码变换的设计者常常面临确保原始程序与变换后程序功能等价性的问题。目前，他们不得不依赖不完整且耗时的仿真。相比之下，针对原始程序对变换后程序进行形式化自动验证更为可取。这就需要类似于用于比较数字电路的等价性检查工具。我们提出了一种这样的工具，用于比较通过表达式传播、循环和代数变换等重要全局变换组合相关联的数组密集型程序。当变换后的程序未能通过等价性检查时，该工具会提供关于可能错误位置的具体反馈。
引用
@article{arxiv.0710.4689,
title = {Functional Equivalence Checking for Verification of Algebraic Transformations on Array-Intensive Source Code},
author = {K. C. Shashidhar and Maurice Bruynooghe and Francky Catthoor and Gerda Janssens},
journal= {arXiv preprint arXiv:0710.4689},
year = {2011}
}
评论
Submitted on behalf of EDAA (http://www.edaa.com/)