循环不变式

作品数：51被引量：83H指数：5
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：薛锦云杨庆红左正康石海鹤游珍更多>>
相关机构：江西师范大学中国科学院软件研究所中国科学技术大学南京大学更多>>
相关期刊：《计算机与数字工程》《计算机与现代化》《西北师范大学学报（自然科学版）》《福州大学学报（自然科学版）》更多>>
相关基金：国家自然科学基金江西省自然科学基金江西省教育厅科学技术研究项目国家重点基础研究发展计划更多>>
-
在结果中检索

检索结果分析

结果分析中...
选择条件：
  • 基金=国家重点基础研究发展计划x
共 条 记 录，以下是1-4
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
用Dixon结式产生非线性循环不变式被引量：1
《四川大学学报（工程科学版）》2012年第4期115-121,共7页余伟 冯勇 
国家"973"计划资助项目(2011CB302402);国家自然科学基金面上项目(11171053);国家自然科学基金重大研究计划资助项目(91118001)
针对循环程序的部分正确性问题,在代数变迁系统理论基础上,结合约束理论提出了一种用Dixon结式生成循环不变式的算法。首先,程序被转换成代数变迁系统,再根据代数变迁关系和不变式模板构造一个多项式组,计算此多项式组的Dixon结式可以...
关键词：循环不变式 Dixon结式 模板 约束 
循环不变式开发技术研究被引量：5
《计算机工程与科学》2010年第9期84-88,94,共6页万松松 薛锦云 谢武平 
国家自然科学基金资助项目(60773054);国家973计划资助项目(2003CCA02800);科技部国际科技合作项目(2008DFA11940)
高可靠性软件是当今软件开发的热点问题。确保算法程序逻辑结构正确最理想的途径是算法程序的形式化推导和证明,而循环不变式是算法程序形式推导和证明的关键。循环不变式的开发一直是算法程序设计领域中最具挑战性、最富有创造性、也...
关键词：循环不变式 PAR方法 高可靠性软件 谓词抽象 
树非递归遍历统一的新解法及其形式证明被引量：1
《江西师范大学学报（自然科学版）》2010年第2期123-127,共5页化志章 杨庆红 揭安全 
国家"973"前期预研项目(2003CCA02800);国家自然科学基金(60273092);江西省自然基金(2008GQS0056);江西省教育厅科技项目(GJJ09142)资助
提出树遍历统一的新解法,使其非递归算法像递归算法一样简单.首先以后序遍历为例,基于结点状态标记和遍历规则提取,从遍历定义导出遍历的递推公式,由此机械获得非递归算法和循环不变式,并用形式化方法证明其正确性.之后按不同遍历定义...
关键词：树遍历 非递归算法 循环不变式 
非线性循环不变式的自动生成被引量：4
《计算机应用》2008年第7期1854-1857,共4页毕忠勤 曾振柄 郭远华 
国家自然科学基金资助项目(90718041);国家973计划项目(2004CB318003);国家863计划项目(2007AA010302);华东师范大学2008年优秀博士生培养基金资助项目(20080029)
提出了一个自动生成非线性循环不变式的算法。循环不变式可以表示成一个带参数的多项式的形式,根据断言的归纳特性,将循环不变式的生成问题转变成一个约束求解问题,这个约束求解问题的每个解对应于一个循环不变式,如果约束求解问题仅有...
关键词：程序验证 循环不变式 变迁系统 约束求解问题 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部