终止性

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

检索结果分析

结果分析中...
选择条件：
  • 期刊=软件学报x
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
单分支线性约束循环程序的终止性分析
《软件学报》2024年第3期1307-1320,共14页李轶 唐桐 
重庆市自然科学基金(cstc2019jcyj-msxmX0638);国家自然科学基金(11771421);中国科学院“西部之光”人才培养计划。
秩函数法是循环终止性分析的主要方法,秩函数的存在表明了循环程序是可终止的.针对单分支线性约束循环程序,提出一种方法对此类循环的终止性进行分析.基于增函数法向空间的计算,该方法将原程序空间上的秩函数计算问题归结为其子空间上...
关键词：循环程序 线性秩函数 增函数 终止性 多阶段秩函数 
PROPER:一个概率程序终止性与正确性分析工具
《软件学报》2022年第12期4464-4475,共12页赵旭慧 邓玉欣 符鸿飞 
国家自然科学基金(62072176,61832015,61802254)。
概率程序将概率推理模型与图灵完备的编程语言相结合,统一了对计算和不确定性知识的形式化描述,能够有效地处理复杂的关系模型和不确定性问题.提供了一种用于分析仿射概率程序的工具PROPER.一方面,它有助于定性和定量地分析仿射概率程...
关键词：概率编程 终止性 断言分析 程序验证 
基于锁耦合遍历算法的文件系统终止性验证被引量：1
《软件学报》2022年第8期2980-2994,共15页邹沫 谢昊彤 魏卓然 陈海波 
国家杰出青年科学基金(61925206)。
并发文件系统由于复杂的实现,容易产生死锁、无限循环等终止性漏洞,已有的文件系统证明工作都忽视了终止性的证明.证明了一个并发文件系统Atom FS的终止性,保证了每个文件系统接口在公平调度的条件下都能返回.证明Atom FS接口的终止性...
关键词：并发文件系统 终止性 形式化验证 COQ 
基于深度学习和反例制导的循环程序秩函数生成
《软件学报》2022年第8期2918-2929,共12页林开鹏 梅国泉 林望 丁佐华 
浙江省自然科学基金(LY20F020020);上海工业控制系统安全创新功能型平台开放课题;上海工业控制安全创新科技有限公司资助课题。
程序终止性判定是程序分析与验证领域中的一个研究热点.针对非线性循环程序,提出了一种基于反例制导的神经网络型秩函数的构造方法.该方法采用学习组件和验证组件交互的迭代框架,其中,学习组件利用程序轨迹作为训练集合构造一个候选秩函...
关键词：秩函数 反例制导方法 深度神经网络 终止性分析 循环程序 
多项式循环程序的秩函数探测
《软件学报》2019年第11期3243-3258,共16页李轶 冯勇 
国家自然科学基金(61572024,61103110,11671377);重庆市自然科学基金(cstc2019jcyj-msxm X0638)~~
秩函数法是循环程序终止性分析的主流方法.针对一类多分支多项式循环程序,这类程序的秩函数计算问题被证明可归结为单形上正定多项式的探测问题,从而便于利用线性规划工具Simplex去计算这类程序的秩函数.不同于现有基于柱形代数分解的...
关键词：可信计算 多分支循环程序 终止性 秩函数 
基于SVM的多项式循环程序秩函数生成被引量：2
《软件学报》2019年第7期1903-1915,共13页李轶 蔡天训 樊建峰 吴文渊 冯勇 
国家自然科学基金(61572024,61103110,11471307)~~
程序终止性问题是自动程序验证领域中的一个研究热点。秩函数探测是进行终止性分析的主要方法。针对单重无条件分支的多项式循环程序,将其秩函数计算问题归结为二分类问题,从而可利用支持向量机(SVM)算法来计算程序的秩函数。与基于量...
关键词：程序终止性 SVM 机器学习 秩函数 
有界闭连通域上的非线性循环终止性分析
《软件学报》2016年第3期517-526,共10页李轶 冯勇 
国家自然科学基金(61572024;61103110;11171053)~~
运用计算机代数中的Groebner基理论,对有界闭连通域上的单重非线性循环程序的终止性问题进行研究,建立了可计算的终止性判定算法.该算法将这类循环的终止性判定问题归约为有无不动点的判定问题.
关键词：可信计算 非线性循环 终止性分析 GROEBNER基 计算机代数 
多分支单变量循环程序的终止性分析
《软件学报》2015年第2期297-304,共8页李轶 李传璨 吴文渊 
国家自然科学基金(61103110);重庆市科技攻关项目(cstc2012gg B40004;cstc2013jjys0002)
对多分支单变量循环程序的终止性问题进行了研究.证明了在适定的条件下,该类循环程序不可终止性的充分必要条件是迭代映射在循环条件形成的区域中有不动点.特别地,当这类循环程序是多项式循环程序时,在给定条件下,其在实数域上的终止性...
关键词：可信计算 多分支循环程序 终止性分析 
有界闭域上的线性赋值循环终止性分析
《软件学报》2014年第6期1133-1142,共10页李轶 吴文渊 冯勇 
国家自然科学基金(61103110);重庆市科技攻关项目(cstc2012ggB40004)
对有界闭域上的线性赋值循环程序终止性问题进行研究.利用Jordan标准型技术将原循环程序的终止性问题约减为终止性等价的具有简单结构的循环程序的终止性问题.证明了当线性迭代映射满足一定条件时,该类循环程序不可终止的充分必要条件是...
关键词：可信计算 非线性循环 终止性分析 JORDAN标准型 有界闭域 
非线性循环的终止性分析被引量：2
《软件学报》2012年第5期1045-1052,共8页李轶 
国家自然科学基金(90718041);上海市高可信计算重点实验室开放课题(07dz22304200801)
单重线性循环程序的终止性问题已被广泛研究,而有关非线性循环终止性判定的结果甚少.利用不动点理论研究了n维单重非线性循环的终止性问题,并建立了相应的符号判定算法.同时,对几类特殊循环的终止性进行了分析,得出了相应的结论.
关键词：可信计算 非线性循环 终止性分析 DISCOVERER 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部