基于吴方法的不变式生成算法

• 作者: 吴尽昭 周宁 王超
• 来源期刊: 北京交通大学学报
• 学科: 工学
• 关键词: 程序验证 不变式生成 符号计算 吴方法
• 年，卷（期）: 2012,（2）
• 所属期刊栏目: 计算机与信息技术
• 页码范围: 1-7
• 分类号: TP301.6
• 字数: 8004字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-0291.2012.02.001

摘要

在并发程序的分析及验证过程中,不变式起着至关重要的作用,为了提高非线性不变式自动生成算法的效率及通用性,基于将非线性不变式生成问题转换为数值约束求解问题的思想,提出通过检验根理想的从属关系方法使算法具备处理通用代数变迁系统的能力；建立了基于吴方法的非线性不变式自动生成算法,该算法不使用加强的归纳条件,并可以直接处理约束方程.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	吴尽昭	北京交通大学计算机与信息技术学院	5	22	3.0	4.0
3	王超	北京交通大学计算机与信息技术学院	46	370	11.0	18.0
6	周宁	北京交通大学计算机与信息技术学院	10	16	3.0	3.0