程序终止性

作品数：9被引量：9H指数：2
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：冯勇李骏李轶李轶纪兆辉更多>>
相关机构：中国科学院大学华东师范大学中国科学院成都计算机应用研究所中国科学院重庆绿色智能技术研究院更多>>
相关期刊：《软件学报》《软件导刊》《计算机工程与应用》《计算机科学》更多>>
相关基金：国家自然科学基金国家重点基础研究发展计划中国科学院知识创新工程重要方向项目更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-9
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于迭代轨迹划分的单分支循环程序终止性分析
《计算机科学》2023年第9期108-116,共9页王垚 李轶 
国家自然科学基金(61572024,11771421,61103110);重庆市自然科学基金(cstc2019jcyj-msxmX0638);重庆市院士专项(cstc2018jcyjyszxX0002,cstc2019yszx-jcyjX0003);国家重点研发计划(2020YFA07123000);中国科学院“西部之光”。
秩函数作为循环程序终止性分析的重要方法已得到广泛研究。文中着重研究了单分支循环的终止性。首先提出了双向迭代循环概念,将单分支循环分为双向迭代循环和非双向迭代循环。其次,针对双向迭代循环程序,建立了一种划分思路,提出了三段...
关键词：程序验证 秩函数 机器学习 程序终止性 
PROPER:一个概率程序终止性与正确性分析工具
《软件学报》2022年第12期4464-4475,共12页赵旭慧 邓玉欣 符鸿飞 
国家自然科学基金(62072176,61832015,61802254)。
概率程序将概率推理模型与图灵完备的编程语言相结合,统一了对计算和不确定性知识的形式化描述,能够有效地处理复杂的关系模型和不确定性问题.提供了一种用于分析仿射概率程序的工具PROPER.一方面,它有助于定性和定量地分析仿射概率程...
关键词：概率编程 终止性 断言分析 程序验证 
基于SVM的多项式循环程序秩函数生成被引量：2
《软件学报》2019年第7期1903-1915,共13页李轶 蔡天训 樊建峰 吴文渊 冯勇 
国家自然科学基金(61572024,61103110,11471307)~~
程序终止性问题是自动程序验证领域中的一个研究热点。秩函数探测是进行终止性分析的主要方法。针对单重无条件分支的多项式循环程序,将其秩函数计算问题归结为二分类问题,从而可利用支持向量机(SVM)算法来计算程序的秩函数。与基于量...
关键词：程序终止性 SVM 机器学习 秩函数 
命令式程序终止性验证方法综述
《计算机工程与应用》2011年第28期1-6,105,共7页李仁见 王昭飞 
国家自然科学基金(No.60725206);国家973项目课题(No.2011CB302603)~~
作为软件完全正确性的重要组成部分,程序终止性受到越来越多的关注。旨在跟踪国内外针对命令式程序的终止性验证方法,调研该领域的最新研究成果,同时提出解决该问题的建议性方法框架,对命令式程序终止性研究提供有意义的帮助。给出了程...
关键词：终止性 命令式程序 秩函数 尺寸变化终止(SCT)分析 模型检验 
线性程序的Ranking函数自动合成被引量：1
《四川大学学报（工程科学版）》2009年第5期176-181,共6页李骏 李轶 冯勇 秦小林 
国家科委973资助项目(2004CB318003);中国科学院知识创新重要方向项目(KJCX2-YW-S02);国家自然科学基金资助项目(10771205);国家自然科学基金资助项目(90718041)
针对判定一个程序终止性的经典方法Ranking函数法,运用半代数系统的概念,把程序终止性问题转换为求半代数系统的Ranking函数。然后运用符号计算工具DISCOV-ERER和Farkas引理,求出函数参数存在的充分必要条件,并根据符号计算理论的方法...
关键词：DISCOVERER Farkas’lemma Ranking函数 半代数系统 程序终止性 程序验证 
基于良序集方法的程序终止性证明
《软件导刊》2009年第6期33-35,共3页彭瑞峰 丁志义 王家伟 
在介绍程序正确性的定义和良序集的概念基础上,对良序集证明程序终止性思路和步骤进行了分析,利用实例来证明程序的终止性。
关键词：良序集 程序正确性 程序证明 程序终止性 
一类循环条件非线性的程序终止性被引量：4
《四川大学学报（工程科学版）》2009年第1期129-133,共5页李骏 李轶 冯勇 
国家科委973资助项目(2004CB318003);中国科学院知识创新重要方向资助项目(KJCX2-YW-S02);国家自然科学基金资助项目(10771205)
针对Tiwari提出的线性循环程序的终止性判定问题,提出了循环条件为齐次多项式的非线性程序的不可中止性判定的理论证明,然后将程序终止性判定问题转化为参数半代数系统的求解。在求解中,借助强有力的代数符号工具DISCOVERER,解决了计算...
关键词：非线性程序 终止性 程序验证 JORDAN标准型 
用Floyd方法证明程序正确性被引量：3
《淮海工学院学报（自然科学版）》2000年第2期1-3,共3页纪兆辉 
介绍 R· W· Floyd关于程序正确性的证明方法 ,并结合一个程序实例 。
关键词：程序终止性 程序正确性 良序集 Floyd方法 
PROLOG的内部谓词cut及其对程序终止性的影响
《计算机工程与应用》1989年第5期60-65,共6页曾抗生 
国家自然科学基金
PROLOG语言中引进了cut这一重要的内部谓词(built-in predicate)。使用cut可以方便地表达出过程性语义中不可缺少的控制结构——选择和循环。并且,cut还有利于提高程序的效率——加快运行速度和节省存储空间。但是,cut并不是原来一阶逻...
关键词：PROLOG语言 谓词Cut 程序终止性 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部