终止性

作品数：103被引量：114H指数：5
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：李轶冯勇吴文渊郝忠孝杨泽雪更多>>
相关机构：中国科学院重庆绿色智能技术研究院哈尔滨理工大学中国科学院大学中国科学院成都计算机应用研究所更多>>
相关期刊：更多>>
相关基金：国家自然科学基金国家重点基础研究发展计划黑龙江省自然科学基金重庆市科技攻关计划更多>>
-
在结果中检索

检索结果分析

结果分析中...
选择条件：
  • 期刊=计算机科学x
共 条 记 录，以下是1-5
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于迭代轨迹划分的单分支循环程序终止性分析
《计算机科学》2023年第9期108-116,共9页王垚 李轶 
国家自然科学基金(61572024,11771421,61103110);重庆市自然科学基金(cstc2019jcyj-msxmX0638);重庆市院士专项(cstc2018jcyjyszxX0002,cstc2019yszx-jcyjX0003);国家重点研发计划(2020YFA07123000);中国科学院“西部之光”。
秩函数作为循环程序终止性分析的重要方法已得到广泛研究。文中着重研究了单分支循环的终止性。首先提出了双向迭代循环概念,将单分支循环分为双向迭代循环和非双向迭代循环。其次,针对双向迭代循环程序,建立了一种划分思路,提出了三段...
关键词：程序验证 秩函数 机器学习 程序终止性 
基于k阶秩函数的线性赋值循环程序的终止性分析
《计算机科学》2018年第6期151-155,共5页李轶 蔡天训 吴文渊 
国家自然科学基金(61572024;61103110;11471307)资助
循环程序的终止性是确保循环程序完全正确的必要条件。如果给定的线性赋值循环程序不存在传统定义的线性秩函数,那么基于传统定义的秩函数终止性证明方法将失效。基于Anx的精确计算,对传统的秩函数概念进行了扩展,提出了k阶秩函数的概...
关键词：线性循环程序 终止性分析 k阶秩函数 RegularChains 
计算最终线性秩函数的新方法
《计算机科学》2017年第1期194-198,213,共6页朱广 李轶 吴文渊 
国家自然科学基金(61572024;11471307);重庆市基础与前沿研究计划院士专项(cstc2015jcyjys40001)资助
程序的终止性分析作为程序验证中重要的一环,在软件正确性验证中极为重要。对于一个线性循环程序,若该程序没有传统定义的线性秩函数,则基于传统定义的秩函数终止性分析方法失效。2013年,Bagnara提出了最终线性秩函数(Eventual Linear R...
关键词：线性循环程序 终止性分析 最终线性秩函数 MATHEMATICA 
基于抽象解释的服务间消息的数据约减被引量：1
《计算机科学》2015年第12期175-180,共6页蒋曹清 肖芳雄 高荣 应时 文静 
国家自然科学基础重点项目(91118003;61272113;61272108);国家自然科学基金项目(61070012;61170022;6126200);广西高校科学技术研究项目(YB2014349)资助
面向服务软件中服务间消息的变量值可能存在无穷域的情况,从而导致模型检测时产生状态空间爆炸问题。为了使终止性验证在实践上可行,需要约减模型状态空间的大小,使得计算时间和空间需求合理。为此,基于抽象解释的区间抽象理论扩展了经...
关键词：抽象解释 终止性验证 模型检测 数据约减 
XML中的主动规则及其可终止性分析
《计算机科学》2004年第9期93-95,共3页李晖 孔兰菊 洪晓光 
主动XML系统一般采用触发器,即"事件-冬件-动作"(ECA)规则来提供主动行为。本文提出了一种新的事件监测机制,在XML系统中引入‘主动节点’,即把规则也融入节点,各节点上的ECA规则只需在节点修改时被激活并进行检查,提高了动作的执行效率...
关键词：XML 递归 主动规则 分析规则 触发 结合规则 可满足性 终止 激活 监测机制 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部