公开(公告)号：CN103617115A

公开(公告)日：2014-03-05

申请号：CN201310529070.1

申请日：2013-10-30

Applicant: 北京信息控制研究所

Inventor： 詹海潭 ,  李宁 ,  张伟 ,  吴世堂 ,  高金梁 ,  郑平

IPC: G06F11/36

Abstract: 一种基于抽象解释和模型验证的运行时错误分析方法，本发明包括以下步骤：基于抽象解释理论，采用前向迭代方法分析程序数值变量值范围，获得程序点达到稳定时的变量值范围信息，对于循环节点的迭代计算采用循环展开和延迟拓宽相结合的方法实现；根据待分析的运行时错误类型，在相关需要检测的程序点处将变量值范围信息转化为断言或假设形式插入程序中；将带有断言和假设的程序转化为布尔公式，其中布尔公式包括限制条件和属性；使用SAT验证器判断布尔公式中属性的正确性。若正确，说明不存在相关运行时错误；若不正确，说明存在相关运行时错误，并输出相关的反例路径。本发明实现了在运行时错误分析精度和效率之间取得一个平衡点。

公开(公告)号：CN103617115B

公开(公告)日：2016-02-10

申请号：CN201310529070.1

申请日：2013-10-30

Applicant: 北京信息控制研究所

Inventor： 詹海潭 ,  李宁 ,  张伟 ,  吴世堂 ,  高金梁 ,  郑平

IPC: G06F11/36

Abstract: 一种基于抽象解释和模型验证的运行时错误分析方法，本发明包括以下步骤：基于抽象解释理论，采用前向迭代方法分析程序数值变量值范围，获得程序点达到稳定时的变量值范围信息，对于循环节点的迭代计算采用循环展开和延迟拓宽相结合的方法实现；根据待分析的运行时错误类型，在相关需要检测的程序点处将变量值范围信息转化为断言或假设形式插入程序中；将带有断言和假设的程序转化为布尔公式，其中布尔公式包括限制条件和属性；使用SAT验证器判断布尔公式中属性的正确性。若正确，说明不存在相关运行时错误；若不正确，说明存在相关运行时错误，并输出相关的反例路径。本发明实现了在运行时错误分析精度和效率之间取得一个平衡点。