数值性质是程序的重要属性之一，不仅仅因为通过分析数值性质可以直接检查程序可能产生的运行时错误（如除零错、算数溢出等），还因为数值分析是许多其他程序分析方法（如别名分析、形态分析等）的基础。程序中非凸数值性质是程序数值分析研究的新热点和难点。抽象解释理论是数值程序分析方面最重要的理论之一，抽象域是抽象解释理论的核心。传统的弱关系型数值抽象域无法表达程序的非凸性质，而可以表达非凸性质的强关系型抽象域有着指数级别的时间复杂度，无法在大规模系统上应用。本文提出一种弱关系型绝对值数值抽象域，它可以表达程序非凸性质且时间复杂度为多项式级别，具有较高的应用价值。本文利用绝对值的天然非凸性，在八边形抽象域中加入绝对值变量，构建了可以描述程序非凸性质的弱关系型绝对值数值抽象域。本文研究了其域表示方法，并提出了三种标准化算子，以满足用户对精度和时间消耗的不同需求。本文还对其中两种标准化算子设计了其增量式算法，进一步降低了时间复杂度。本文对弱关系型绝对值数值抽象域设计了完整的域操作，包括格相关操作，迁移函数，加宽/变窄算子等。在此基础上，在开源数值抽象域库APRON中实现了该抽象域的所有域操作。本文搭建了以Interproc为前端、APRON为抽象域库、Fixpoint为不动点求解器的面向Spl语言的实验平台。还研究了benchmark的选取方法，基于公正性、透明性、多样性、适应性、典型性的原则选取了大小不一的12组测试样例。基于搭建的实验平台，本文对弱关系型绝对值数值抽象域的三种标准化算子、弱关系型绝对值数值抽象域与八边形抽象域和线性绝对值不等式抽象域的精度和时间消耗进行了对比分析。实验结果表明，弱关系型绝对值数值抽象域可以表达程序非凸数值性质，且在精度和时间消耗上有着很好的均衡，具有较好的理论和实际意义。