基于抽象解释的不变式验证
通常程序的不变式验证可转化为不动点求解问题,但直接计算不动点是非常困难的,故验证时态性质p 常依赖于找到合适地辅助不变式q,使之满足Reach(M)(∈)”q”(∈)”p”。本文提出了两种解决方法：(1)基于抽象解释及不动点抽象定理,在抽象域中通过前向或逆向转换求解抽象不动点,并采用widening和narrowing 操作加速收敛,从而完成不变式的自动验证。(2)通过Tableau 方法构造所验证时态公式的谓词图,采用状态前向或逆向转换,改进了不变式验证的规则,并基于抽象解释框架,通过模拟构造抽象状态转换系统,给出了不变式验证的抽象规则。
抽象解释 不动点 不变式验证 可达性 模拟
钱俊彦 郭云川 赵岭忠 蔡国永
国防科学技术大学计算机学院博士后流动站,湖南 长沙 410073 中国科学院信息工程研究所,北京 100093 桂林电子科技大学 广西可信软件重点实验室,广西 桂林 541004
国内会议
南京
中文
1-16
2012-10-20（万方平台首次上网日期，不代表论文的发表时间）