目前,软件应用已经渗透到人们生活的方方面面,软件质量已经引起人们普遍关注。程序作为软件的核心,其正确性是保证软件质量的前提。程序数值变量取值范围分析在程序验证中占据重要地位,通过对变量取值范围静态分析可以检测到程序测试中不易发现的问题,从而避免程序运行时相关错误发生。抽象解释为程序静态分析提供了一个理论框架。基于抽象解释理论,本课题研究了区间和八边形两种抽象解释域。在此基础上,设计开发相关的静态检测工具实现对C语言程序中变量取值范围分析。具体创新性与主要工作成果如下:(1)针对目前存在的基于区间抽象域的变量值范围分析方法存在的代码覆盖率不高问题,提出了一种改进的分析变量取值区间方法。基于此方法,实现一个检验程序变量数值性质的工具。该工具全面考虑了不同语句结构的相互嵌套,找到数值型程序中存在的矛盾结点,同时兼顾了效率与分析精度问题。(2)基于八边形抽象域理论设计并实现了一个数值程序分析的检测工具。该工具通过对程序中的语法结构进行建模和抽象,计算出程序变量的上下文状态,从而判断程序变量范围是否满足需求。该工具能够有效地检验程序中是否存在某些运行时错误,并在正确性和计算效率之间达到一个较好的平衡。