非线性循环不变式的自动生成

• 作者: 曾振柄 毕忠勤 郭远华
• 来源期刊: 计算机应用
• 学科: 工学
• 关键词: 程序验证 循环不变式 变迁系统 约束求解问题
• 年，卷（期）: 2008,（7）
• 所属期刊栏目: 典型应用
• 页码范围: 1854-1857
• 页数: 4页
• 分类号: TP311.1
• 字数: 5778字
• 语种: 中文

摘要

提出了一个自动生成非线性循环不变式的算法.循环不变式可以表示成一个带参数的多项式的形式,根据断言的归纳特性,将循环不变式的生成问题转变成一个约束求解问题,这个约束求解问题的每个解对应于一个循环不变式,如果约束求解问题仅有零解,则说明不存在该参数多项式形式的循环不变式.该算法在Maple中得到了实现,并通过一些实例说明了该算法的有效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	毕忠勤	华东师范大学上海市高可信计算重点实验室	5	13	2.0	3.0
2	曾振柄	华东师范大学上海市高可信计算重点实验室	29	105	6.0	8.0
3	郭远华	华东师范大学上海市高可信计算重点实验室	6	13	2.0	3.0