汤震浩

作品数：4被引量：8H指数：2
导出分析报告
供职机构：计算机软件新技术国家重点实验室更多>>
发文主题：变式循环不变式自动生成方法数组一致性更多>>
发文领域：自动化与计算机技术更多>>
发文期刊：《软件学报》更多>>
所获基金：国家自然科学基金国家重点基础研究发展计划更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-4
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
自动分析递归数据结构的归纳性质被引量：2
《软件学报》2018年第6期1527-1543,共17页汤震浩 李彬 翟娟 赵建华 
国家重点研发计划(2016YFB1000802);国家自然科学基金(61632015;61561146394)~~
提出了一种对递归数据结构的归纳性质进行自动化分析的框架.工作分为3个主要部分.首先,它将递归数据结构的归纳性质分为两个主要类别,并提出对应的处理模式,从而帮助简化对于程序中的递归数据结构上的相关性质的分析.其次,提出了一种称...
关键词：霍尔式程序证明 程序分析 递归数据结构 归纳性质 过程间分析 
自动合成数组不变式被引量：3
《软件学报》2018年第6期1544-1565,共22页李彬 翟娟 汤震浩 汤恩义 赵建华 
国家自然科学基金(61632015;61561146394);国家重点研发计划(2016YFB1000802)~~
提出了基于抽象解释框架自动合成数组程序不变式的方法,它能够分析按照特定顺序访问一维或者多维数组的程序,然后合成不变式.该方法将性质(包括区间全称量词性质和原子性质)集合作为抽象域,通过前向迭代数据流分析合成数组性质.证明了...
关键词：不变式合成 抽象解释 数组程序 
常用循环摘要的自动生成方法及其应用被引量：3
《软件学报》2017年第5期1051-1069,共19页翟娟 汤震浩 李彬 赵建华 李宣东 
国家自然科学基金(61632015;61561146394);国家重点研发计划(2016YFB1000802)~~
采用形式化方法证明软件的正确性,是保障软件可靠性的有效方法.而对循环语句的分析与验证,是形式化证明中的关键,对循环语句的处理一直是程序分析与验证中的一个难点问题.提出使用循环语句修改的内存和这些内存中存放的新值来描述循环...
关键词：循环摘要 循环不变式 前置条件 后置条件 程序验证 
通过抽象程序证明复杂具体程序被引量：2
《软件学报》2017年第4期786-803,共18页李彬 汤震浩 翟娟 赵建华 
国家自然科学基金(61632015;61561146394);国家重点基础研究发展计划(973)(2016YFB1000802)~~
描述了证明抽象程序和具体程序满足一致性关系的方法.抽象程序使用抽象数据结构(ADTs),如set,list,map及其上的操作.具体程序使用类C语言中的类型.抽象程序和具体程序一致性证明需要用户给出抽象变量和具体变量的关系、抽象程序程序点...
关键词：程序证明 一致性 抽象程序 精化 分解 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部