首页> 中文会议>第十一届全国软件与应用学术会议（NASAC2012） >基于抽象解释的不变式验证

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

页面导航

摘要
著录项
相似文献
相关主题

摘要

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

著录项

来源
《第十一届全国软件与应用学术会议（NASAC2012）》|2012年|1-16|共16页
会议地点南京
作者
QIAN Jun-yan; 钱俊彦; GUO Yun-chuan; 郭云川; ZHAO Ling-zhong; 赵岭忠; CAI Guo-yong; 蔡国永;
展开▼
作者单位

中国计算机学会;

展开▼
会议组织
正文语种
原文格式 PDF
中图分类程序设计;
关键词
程序设计; 不变式验证; 抽象解释; 时态性质;

相似文献

中文文献
外文文献
专利

1. 基于抽象解释的函数不变量正确性验证 [J] . 武书彦 ,苏青琴 ,刘久富 . 微电子学与计算机 . 2012,第10期
2. 基于抽象解释理论的程序验证技术 [J] . 李梦君 ,李舟军 ,陈火旺 . 软件学报 . 2008,第001期
3. 基于抽象解释的Prolog程序验证技术研究 [J] . 赵岭忠 ,古天龙 ,蔡国永 . 计算机科学 . 2008,第007期
4. 基于流分析与归纳不变式结合的German协议验证 [J] . 张瑜 ,孙文辉 . 计算机系统应用 . 2017,第010期
5. 基于不变式生成的循环停机性验证 [J] . 邢建英 ,李梦君 ,李舟军 . 计算机工程与科学 . 2012,第004期
6. 基于抽象解释的不变式验证 [C] . ZHANG Yan ,张 ,QIAN Junyan . 第八届信息安全漏洞分析与风险评估大会 . 2015
7. 基于两区间抽象域的抽象解释方法研究与实现 [A] . 丁泽文 . 2017

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

摘要

著录项

相似文献

相关主题

期刊订阅