终止性

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

检索结果分析

结果分析中...
条 记 录,以下是1-10
视图:
排序:
单分支线性约束循环程序的终止性分析
《软件学报》2024年第3期1307-1320,共14页李轶 唐桐 
重庆市自然科学基金(cstc2019jcyj-msxmX0638);国家自然科学基金(11771421);中国科学院“西部之光”人才培养计划。
秩函数法是循环终止性分析的主要方法,秩函数的存在表明了循环程序是可终止的.针对单分支线性约束循环程序,提出一种方法对此类循环的终止性进行分析.基于增函数法向空间的计算,该方法将原程序空间上的秩函数计算问题归结为其子空间上...
关键词:循环程序 线性秩函数 增函数 终止性 多阶段秩函数 
基于迭代轨迹划分的单分支循环程序终止性分析
《计算机科学》2023年第9期108-116,共9页王垚 李轶 
国家自然科学基金(61572024,11771421,61103110);重庆市自然科学基金(cstc2019jcyj-msxmX0638);重庆市院士专项(cstc2018jcyjyszxX0002,cstc2019yszx-jcyjX0003);国家重点研发计划(2020YFA07123000);中国科学院“西部之光”。
秩函数作为循环程序终止性分析的重要方法已得到广泛研究。文中着重研究了单分支循环的终止性。首先提出了双向迭代循环概念,将单分支循环分为双向迭代循环和非双向迭代循环。其次,针对双向迭代循环程序,建立了一种划分思路,提出了三段...
关键词:程序验证 秩函数 机器学习 程序终止性 
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);上海工业控制系统安全创新功能型平台开放课题;上海工业控制安全创新科技有限公司资助课题。
程序终止性判定是程序分析与验证领域中的一个研究热点.针对非线性循环程序,提出了一种基于反例制导的神经网络型秩函数的构造方法.该方法采用学习组件和验证组件交互的迭代框架,其中,学习组件利用程序轨迹作为训练集合构造一个候选秩函...
关键词:秩函数 反例制导方法 深度神经网络 终止性分析 循环程序 
指数函数多项式的实根分离算法被引量:1
《计算机应用》2022年第5期1531-1537,共7页葛昕钰 陈世平 刘忠 
四川省科学技术厅科技计划项目(2016GFW0048)。
针对超越函数多项式的实根分离问题,提出了一种指数函数多项式的区间分离算法exRoot,将非多项式型实函数的实根分离问题转化为多项式正负性判定问题进而对其求解。首先,利用泰勒替换法构造目标函数的多项式区间套;然后,将指数函数的求...
关键词:指数函数多项式 实根分离 泰勒替换法 区间列 终止性 
循环程序的界函数合成
《计算机应用》2022年第2期565-573,共9页谭旺 李轶 
国家自然科学基金资助项目(11771421);中国科学院“西部之光”;国家重点研发计划项目(2020YFA07123000);重庆市自然科学基金资助项目(cstc2019jcyj-msxmX0638)。
作为循环程序终止性分析的主流方法,当前的秩函数方法大多局限于线性或多项式秩函数的求解。针对循环程序若不存在对应的线性或多项式秩函数,现有秩函数方法就无法证明其终止性的问题,提出一个新的方法来合成给定循环程序对应的界函数...
关键词:程序验证 循环程序终止性 支持向量机 界函数 秩函数 
多项式循环程序的秩函数探测
《软件学报》2019年第11期3243-3258,共16页李轶 冯勇 
国家自然科学基金(61572024,61103110,11671377);重庆市自然科学基金(cstc2019jcyj-msxm X0638)~~
秩函数法是循环程序终止性分析的主流方法.针对一类多分支多项式循环程序,这类程序的秩函数计算问题被证明可归结为单形上正定多项式的探测问题,从而便于利用线性规划工具Simplex去计算这类程序的秩函数.不同于现有基于柱形代数分解的...
关键词:可信计算 多分支循环程序 终止性 秩函数 
基于SVM的多项式循环程序秩函数生成被引量:2
《软件学报》2019年第7期1903-1915,共13页李轶 蔡天训 樊建峰 吴文渊 冯勇 
国家自然科学基金(61572024,61103110,11471307)~~
程序终止性问题是自动程序验证领域中的一个研究热点。秩函数探测是进行终止性分析的主要方法。针对单重无条件分支的多项式循环程序,将其秩函数计算问题归结为二分类问题,从而可利用支持向量机(SVM)算法来计算程序的秩函数。与基于量...
关键词:程序终止性 SVM 机器学习 秩函数 
基于Dixon结式和逐次差分代换的多项式秩函数探测方法
《计算机应用》2019年第7期2065-2073,共9页袁月 李轶 
国家自然科学基金资助项目(61472429,61572024,61103110)~~
秩函数探测是循环程序终止性分析的重要方法,目前,已有很多研究者致力于为线性循环程序探测对应的线性秩函数,然而,针对具有多项式循环条件和多项式赋值的多项式型的循环,现有的秩函数探测方法还有所不足,解决方案大多是不完备的、或者...
关键词:循环程序终止性 多项式循环程序 多项式秩函数 多阶段秩函数 Dixon结式 逐次差分代换 
检索报告 对象比较 聚类工具 使用帮助 返回顶部