终止性分析

作品数：27被引量：35H指数：3
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：李轶杨泽雪吴文渊窦文阳张立臣更多>>
相关机构：中国科学院重庆绿色智能技术研究院陕西师范大学重庆邮电大学哈尔滨理工大学更多>>
相关期刊：《通信学报》《计算机应用与软件》《系统科学与数学》《哈尔滨理工大学学报》更多>>
相关基金：国家自然科学基金重庆市科技攻关计划国家重点基础研究发展计划黑龙江省自然科学基金更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于迭代轨迹划分的单分支循环程序终止性分析
《计算机科学》2023年第9期108-116,共9页王垚 李轶 
国家自然科学基金(61572024,11771421,61103110);重庆市自然科学基金(cstc2019jcyj-msxmX0638);重庆市院士专项(cstc2018jcyjyszxX0002,cstc2019yszx-jcyjX0003);国家重点研发计划(2020YFA07123000);中国科学院“西部之光”。
秩函数作为循环程序终止性分析的重要方法已得到广泛研究。文中着重研究了单分支循环的终止性。首先提出了双向迭代循环概念,将单分支循环分为双向迭代循环和非双向迭代循环。其次,针对双向迭代循环程序,建立了一种划分思路,提出了三段...
关键词：程序验证 秩函数 机器学习 程序终止性 
基于深度学习和反例制导的循环程序秩函数生成
《软件学报》2022年第8期2918-2929,共12页林开鹏 梅国泉 林望 丁佐华 
浙江省自然科学基金(LY20F020020);上海工业控制系统安全创新功能型平台开放课题;上海工业控制安全创新科技有限公司资助课题。
程序终止性判定是程序分析与验证领域中的一个研究热点.针对非线性循环程序,提出了一种基于反例制导的神经网络型秩函数的构造方法.该方法采用学习组件和验证组件交互的迭代框架,其中,学习组件利用程序轨迹作为训练集合构造一个候选秩函...
关键词：秩函数 反例制导方法 深度神经网络 终止性分析 循环程序 
基于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 
有界闭连通域上的非线性循环终止性分析
《软件学报》2016年第3期517-526,共10页李轶 冯勇 
国家自然科学基金(61572024;61103110;11171053)~~
运用计算机代数中的Groebner基理论,对有界闭连通域上的单重非线性循环程序的终止性问题进行研究,建立了可计算的终止性判定算法.该算法将这类循环的终止性判定问题归约为有无不动点的判定问题.
关键词：可信计算 非线性循环 终止性分析 GROEBNER基 计算机代数 
多分支单变量循环程序的终止性分析
《软件学报》2015年第2期297-304,共8页李轶 李传璨 吴文渊 
国家自然科学基金(61103110);重庆市科技攻关项目(cstc2012gg B40004;cstc2013jjys0002)
对多分支单变量循环程序的终止性问题进行了研究.证明了在适定的条件下,该类循环程序不可终止性的充分必要条件是迭代映射在循环条件形成的区域中有不动点.特别地,当这类循环程序是多项式循环程序时,在给定条件下,其在实数域上的终止性...
关键词：可信计算 多分支循环程序 终止性分析 
一类带初始输入的线性循环终止性分析
《四川大学学报（工程科学版）》2014年第5期81-87,共7页李轶 李传璨 吴文渊 
国家自然科学基金资助项目(61103110);重庆市科技攻关重点项目(cstc2012ggB40004)
针对带初始输入的2维齐次线性循环的终止性问题进行研究。通过分析该类循环所有非终止点组成集合(即NT集)的性质,将该类循环NT集的构造问题转化为一类非线性优化求解问题,并给出了此类优化问题的数学模型。最终,通过验证该类循环的初始...
关键词：可信软件 循环终止性 最优化问题 QEPCAD 
有界闭域上的线性赋值循环终止性分析
《软件学报》2014年第6期1133-1142,共10页李轶 吴文渊 冯勇 
国家自然科学基金(61103110);重庆市科技攻关项目(cstc2012ggB40004)
对有界闭域上的线性赋值循环程序终止性问题进行研究.利用Jordan标准型技术将原循环程序的终止性问题约减为终止性等价的具有简单结构的循环程序的终止性问题.证明了当线性迭代映射满足一定条件时,该类循环程序不可终止的充分必要条件是...
关键词：可信计算 非线性循环 终止性分析 JORDAN标准型 有界闭域 
基于自依赖规则分析的主动规则终止性研究
《计算机工程与科学》2013年第8期135-143,共9页陆惠玲 周涛 
国家自然科学基金资助项目(81160183);教育部"春晖计划"资助项目(Z2011051);宁夏自然科学基金资助项目(NZ12179);宁夏高等学校科研重点资助项目(NGY2011042);宁夏医科大学特殊人才项目(XT2011004);宁夏医科大学青年基金资助项目(XQ2011011)
ECA规则终止性问题是主动数据库中一个关键问题,首先分析触发边、活化边、惰化边三种边的触发时序关系;然后构造条件断言函数来描述活化边和惰化边对ECA规则中条件的影响,总结出了触发边、活化边和惰化边的组合时序对规则的具体触发情况...
关键词：主动规则 终止性分析 自依赖规则 不可归约规则集 
线性循环程序的终止性判定被引量：1
《系统科学与数学》2013年第5期626-638,共13页李轶 
国家自然科学基金(61103110);国家自然科学基金重点项目(91018012);国家973计划项目(2011CB302400);重庆市科技攻关项目(cstc2012ggB40004)资助课题
对赋值矩阵仅为一个Jordan块的特殊线性循环,构造了不可终止点集的一个子集,证明了此类循环的终止性可仅由该子集是否为空来判定.除此之外,该类循环的终止性被证明也可通过比较几个系数的符号来判定.而对一般的线性循环程序,提出了递归...
关键词：可信计算 线性循环 终止性分析 N-不可终止点 
全选清除导出
共3页<123>
检索报告 对象比较 聚类工具 使用帮助 返回顶部