文档名：基于抽象解释的不变式验证
通常程序的不变式验证可转化为不动点求解问题,但直接计算不动点是非常困难的,故验证时态性质p常依赖于找到合适的辅助不变式q,使之满足Reach(M)(∈)[q](∈)[p].本文提出了两种解决方法:(1)基于抽象解释及不动点抽象定理,在抽象域中通过前向或逆向转换求解抽象不动点,并采用widening和narrowing操作加速收敛,从而完成不变式的自动验证.(2)通过Tableau方法构造所验证时态公式的谓词图,采用状态前向或逆向转换,改进了不变式验证的规则,并基于抽象解释框架,通过模拟构造抽象状态转换系统,给出了不变式验证的抽象规则.
作者：张 钱俊彦 李舟军 马殿富
作者单位：北京航空航天大学计算机学院,北京100085;湖北大学计算机与信息工程学院,武汉430062桂林电子科技大学计算机科学学院,桂林541004北京航空航天大学计算机学院,北京100085
母体文献：第八届信息安全漏洞分析与风险评估大会论文集
会议名称：第八届信息安全漏洞分析与风险评估大会
会议时间：2015年10月23日
会议地点：北京
主办单位：中国信息安全测评中心
语种：chi
分类号：
关键词：应用程序 不变式验证 抽象解释 不动点抽象定理
在线出版日期：2016年6月21日
基金项目：
相似文献
相关博文
- 文件大小:
- 506.89 KB
- 下载次数:
- 60
-
高速下载
|
|
