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

关键词：静态分析 抽象解释 值范围分析 数值抽象域 数组抽象 

单位：并行与分布处理国防科技重点实验室 湖南长沙410073