摘要
在并发程序的分析及验证过程中,不变式起着至关重要的作用,为了提高非线性不变式自动生成算法的效率及通用性,基于将非线性不变式生成问题转换为数值约束求解问题的思想,提出通过检验根理想的从属关系方法使算法具备处理通用代数变迁系统的能力;建立了基于吴方法的非线性不变式自动生成算法,该算法不使用加强的归纳条件,并可以直接处理约束方程.
For the analysis and verification of concurrent program,invariant is a very important concept.In order to improve the efficiency and generality for non-linear invariant generation algorithm,this paper shows how to convert a non-linear invariant generation problem to a numerical constraint solving problem according to the radical membership of the corresponding ideal.A novel algorithm based on the Wu’s method is proposed,which does not use the stronger condition to solve the inductive assertion,and it can get solutions of constraint equation directly.
出处
《北京交通大学学报》
CAS
CSCD
北大核心
2012年第2期1-7,共7页
JOURNAL OF BEIJING JIAOTONG UNIVERSITY
基金
国家自然科学基金资助项目（63873118,60973147）
教育部博士点基金项目资助（200900009110006）
广西自然科学基金项目资助（2011GxNSFA018154）
广西区主席科技资金资助（10169.1）
广西教育厅科研资助项目资助（201012MS274）
广西混杂计算与集成电路设计分析重点实验室开放基金项目资助（HCIC201102）
关键词
程序验证
不变式生成
符号计算
吴方法
program verification
invariant generation
symbolic computation
WU’s method
