基于抽象解释和数值熵的数值程序分析方法

摘要

在高度依赖软件的信息时代，程序的正确性验证问题需要深入研究。文中提出了基于抽象解释和数值熵的数值程序正确性分析方法。抽象解释理论为程序静态分析提供了一个通用框架，在编译时能够自动地推导程序的动态性质。数值信息熵能够反映变量的值范围，通过熵值的大小可以判断变量取值是否在规定范围内。通过一个C程序对该方法进行了验证，该数值程序分析方法可以做到对程序正确性等的验证，并且较单纯地抽象解释近似分析，正确性、可靠性更高。%In the information age,software is highly dependent,thus the correctness of the program validation issues need to be further study. In the paper,introduce the value range analysis method based on abstract interpretation and value information entropy. The abstract interpretation as an important method of the static analysis,uses testing framework to deduce the program's dynamic property automati-cally. The value information entropy can reflect the range of a variable,through the entropy,can judge whether variable values within the prescribed scope. Through validating this method with C program,find the method can validate the correctness of the running program. Compared with the only abstract interpretation analysis,the method is higher in validity and reliability.