罗奇鸣

作品数：13被引量：9H指数：2
导出分析报告
供职机构：中国科学技术大学计算机科学与技术学院更多>>
发文主题：HOARE逻辑别名英文软件工程GIBBS抽样更多>>
发文领域：自动化与计算机技术生物学更多>>
发文期刊：《小型微型计算机系统》《生物物理学报》《电子技术（上海）》《中国科学技术大学学报》更多>>
所获基金：国家自然科学基金国家教育部博士点基金更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
一种基于栈区内存模型的C程序别名判断算法被引量：1
《小型微型计算机系统》2019年第2期353-358,共6页常欢 罗奇鸣 李薛剑 陈意云 
国家自然科学基金项目(61170018;61229201)资助
C语言中的指针导致C程序中会出现表达式别名的情况.在基于演绎推理的程序验证中,使用Hoare逻辑的赋值规则前必须消除断言中的别名.别名增加了程序验证的难度.本文根据C语言的语义提出了一种栈区内存模型,可以精确地跟踪栈区的多种类型...
关键词：程序验证 HOARE逻辑 内存模型 别名 栈区 
安全C语言验证器中形状系统的形状检查方法被引量：1
《小型微型计算机系统》2019年第1期133-140,共8页孙科 罗奇鸣 李薛剑 陈意云 
国家自然科学基金项目(61170018;61229201)资助
在一个基于霍尔逻辑和形状图逻辑的C语言自动验证器中,设计并实现了对形状图中所含易变数据结构的形状检查方法.本工作在验证器的形状系统中实现了显式形状检查与隐式形状检查,并通过引入不同的形状级别,使验证器能够根据不同的严格程...
关键词：程序验证 形状图逻辑 形状系统 形状检查 
易变数据结构归纳引理的自动证明
《电子技术（上海）》2017年第6期61-66,58,共7页杨晨 罗奇鸣 李薛剑 陈意云 
程序性质的自动验证有时需要验证者提供相关的归纳引理,程序验证的结果可靠与否依赖于验证者所提供的归纳引理正确与否。本文围绕操作易变数据的程序的自动验证,设计并实现一个相关引理的自动证明器,作为程序自动验证器中检查验证者所...
关键词：程序验证 易变数据结构 结构归纳 自动定理证明 
二叉树程序循环不变形状图的自动推断被引量：2
《小型微型计算机系统》2017年第5期913-918,共6页李云龙 罗奇鸣 陈意云 
国家自然科学基金项目(61170018;61229201)资助
在一个基于形状图逻辑的C语言程序自动验证系统上,设计并实现了二叉树形状程序的循环不变形状图的自动推断方法.该方法与单链表程序循环不变形状图的推断方法的区别在于通过增加二叉树形状的等价和蕴含规则,使得在形状图的演算时支持二...
关键词：程序验证 形状图逻辑 形状分析 二叉树 循环不变形状图的自动推断 
关于断言语言中引入逻辑变量的研究被引量：2
《小型微型计算机系统》2017年第5期925-929,共5页李为胜 罗奇鸣 陈意云 
国家自然科学基金项目(61170018;61229201)资助
基于Hoare逻辑推理规则去验证程序安全性的研究是程序验证领域的重要发展方向.但是在Hoare逻辑中,仅依靠程序变量的断言语言无法表达程序上下文中不变性质.本文研究通过在断言语言中引入逻辑变量的方式来表达程序上下文不变性质,同时详...
关键词：HOARE逻辑 形式化验证 逻辑变量 断言语言 
栈指针程序的形式验证被引量：2
《小型微型计算机系统》2017年第5期936-940,共5页冯峰 罗奇鸣 陈意云 
国家自然科学基金项目(61170018;61229201)资助
提出一种验证含栈指针、静态区指针操作的C语言程序的方法.该方法定义指针的三元属性表示一个指针的状态.指针的三元属性包括指针指向数据块的名称、数据块的长度以及指针在所指向数据块上的偏移.通过对Hoare逻辑的扩展,基于指针的三元...
关键词：程序验证 栈指针 静态区指针 路径别名 HOARE逻辑 
基于闭半环的若干图算法
《小型微型计算机系统》2015年第12期2671-2674,共4页罗奇鸣 
MOE-MS多媒体计算与通信实验室基金项目(07122807)资助
闭半环是在半环上添加了传递闭包运算符而得到的代数结构.闭半环为计算机科学理论中多个看起来不相关的问题提供了统一的求解理论框架.有不少图算法问题可以通过对图的邻接矩阵在特定的闭半环上计算闭包而求解.本文分析了三个典型的问题...
关键词：闭半环 图算法 闭包 HASKELL 
一种构件系统重新配置协议的关系逻辑模型
《小型微型计算机系统》2014年第12期2686-2690,共5页罗奇鸣 
MOE-MS多媒体计算与通信实验室基金项目(07122807)资助
基于构件的软件系统在运行过程中需要适应环境和用户需求的变化对自身的结构进行动态的重新配置.本文提出了一个用形式化语言Alloy实现的求解重新配置协议的关系逻辑模型.该模型定义了构件和连接的各种状态,状态之间的转换操作,和每种...
关键词：构件 重新配置 关系逻辑 ALLOY 软件体系结构 
一种利用Kodkod约束求解器验证UML-OCL类图的方法被引量：1
《小型微型计算机系统》2014年第2期205-209,共5页罗奇鸣 
MOE-MS多媒体计算与通信实验室基金项目(07122807)资助
采用形式化方法对软件模型进行自动验证在模型驱动架构开发方法中发挥重要的作用.本文提出一种对面向对象软件设计模型的静态结构进行验证的具体实现方法.该方法将用OCL不变式约束的UML类图转换为用关系逻辑表达的公式,Kodkod约束求解...
关键词：统一建模语言 对象约束语言 类图 验证 软件工程 
综合利用语句和序列可疑度的软件故障定位方法
《小型微型计算机系统》2013年第2期324-327,共4页罗奇鸣 
自动故障定位对于提高软件调试的效率有重要意义.本文提出利用语句、数据流和控制流的频谱信息并基于局部最优性生成和计算语句序列的可疑度,并综合语句所在序列的可疑度和语句的可疑度以获得语句的最终可疑度排序.在西门子测试程序集...
关键词：软件故障定位 语句序列可疑度 程序分析 软件调试 软件工程 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部