基于吴方法的不变式生成算法
周宁1
吴尽昭2
王超3
1.北京交通大学计算机与信息技术学院,北京100044;兰州交通大学数理与软件工程学院,甘肃兰州7300702.北京交通大学计算机与信息技术学院,北京100044;广西民族大学广西混杂计算与集成电路设计分析重点实验室,广西南宁5300063.北京交通大学计算机与信息技术学院,北京,100044
摘要：在并发程序的分析及验证过程中,不变式起着至关重要的作用,为了提高非线性不变式自动生成算法的效率及通用性,基于将非线性不变式生成问题转换为数值约束求解问题的思想,提出通过检验根理想的从属关系方法使算法具备处理通用代数变迁系统的能力；建立了基于吴方法的非线性不变式自动生成算法,该算法不使用加强的归纳条件,并可以直接处理约束方程.
关键词：程序验证不变式生成符号计算吴方法
分类号：TP301.6(计算技术、计算机技术)
资助基金：国家自然科学基金(63873118,60973147)高等学校博士学科点专项科研基金(20090009110006)广西自然科学基金(2011GXNSFA018154)广西区主席科技资金资助(10169-1)广西教育厅科学研究项目(201012MS274)广西混杂计算与集成电路设计分析重点实验室开放基金(HCIC201102)
论文发表日期：2012-01-01
在线出版日期：2025-08-15（本平台首次上网日期，不代表文献的发表时间）
页数：7( 1-7 )
英文信息