| 基于吴方法的不变式生成算法 | |
| 周宁 ; 吴尽昭 ; 王超 | |
| 2015-03-16 ; 2015-03-16 | |
| 关键词 | 程序验证 不变式生成 符号计算 吴方法 |
| 其他题名 | Invariant generation algorithm based on WU's method |
| 中文摘要 | 在并发程序的分析及验证过程中,不变式起着至关重要的作用,为了提高非线性不变式自动生成算法的效率及通用性,基于将非线性不变式生成问题转换为数值约束求解问题的思想,提出通过检验根理想的从属关系方法使算法具备处理通用代数变迁系统的能力；建立了基于吴方法的非线性不变式自动生成算法,该算法不使用加强的归纳条件,并可以直接处理约束方程.; 国家自然科学基金资助项目(63873118,60973147);教育部博士点基金项目资助(20090009110006);广西自然科学基金项目资助(2011GXNSFA018154);广西区主席科技资金资助(10169-1);广西教育厅科研资助项目资助(201012MS274);广西混杂计算与集成电路设计分析重点实验室开放基金项目资助(HCIC201102) |
| 语种 | 中文 |
| 出版者 | 北京交通大学学报 |
| 其他责任者 | 北京交通大学计算机与信息技术学院 ; 兰州交通大学数理与软件工程学院 ; 广西民族大学广西混杂计算与集成电路设计分析重点实验室 |
| 内容类型 | 期刊论文 |
| 源URL | [http://ir.calis.edu.cn/hdl/530500/4595]  |
| 专题 | 广西民族大学 |
| 推荐引用方式 GB/T 7714 | 周宁,吴尽昭,王超. 基于吴方法的不变式生成算法[J],2015, 2015. |
| APA | 周宁,吴尽昭,&王超.(2015).基于吴方法的不变式生成算法.. |
| MLA | 周宁,et al."基于吴方法的不变式生成算法".(2015). |
| 个性服务 |
| 查看访问统计 |
| 相关权益政策 |
| 暂无数据 |
| 收藏/分享 |
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论