基于抽象解释的不变式验证

摘要：

通常程序的不变式验证可转化为不动点求解问题,但直接计算不动点是非常困难的,故验证时态性质p常依赖于找到合适的辅助不变式q,使之满足Reach(M)(∈)”q”(∈)”p”.本文提出了两种解决方法:(1)基于抽象解释及不动点抽象定理,在抽象域中通过前向或逆向转换求解抽象不动点,并采用widening和narrowing操作加速收敛,从而完成不变式的自动验证.(2)通过Tableau方法构造所验证时态公式的谓词图,采用状态前向或逆向转换,改进了不变式验证的规则,并基于抽象解释框架,通过模拟构造抽象状态转换系统,给出了不变式验证的抽象规则.

关键词： 应用程序 不变式验证 抽象解释 不动点抽象定理

作者: 张 钱俊彦 李舟军 马殿富

作者单位: 北京航空航天大学计算机学院,北京100085 ;湖北大学计算机与信息工程学院,武汉430062 桂林电子科技大学计算机科学学院,桂林541004 北京航空航天大学计算机学院,北京100085

会议类型: 国内会议

会议名称: 第八届信息安全漏洞分析与风险评估大会

会议地点: 北京

会议语种:中文

页码: 110-123

在线出版日期: 2015-10-23（万方平台首次上网日期，不代表论文的发表时间）