论文部分内容阅读
程序的正确性验证一直以来都是计算机科学中的一个挑战性问题，抽象解释理论为程序静态分析提供了一个通用框架，可以在编译时自动地推导程序的动态性质。基于抽象解释的数值程序分析可以自动推导程序中数值变量间的不变式关系，这对于编译优化、程序错误检查至关重要。本文建立并实现了一个面向C和Fortran程序并支持过程间分析的数值程序分析框架和工具，C或Fortran源程序经过预处理后转化为具有统一格式的中间表示形式，然后基于该中间表示抽取与源程序语义等价的语义等式，最后在该语义等式上进行不动点迭代计算从而得到程序不变式