导读:本文包含了循环不变式论文开题报告文献综述及选题提纲参考文献，主要关键词:抽象解释,抽象域,不变式,析取语义
循环不变式论文文献综述
潘建东,陈立前,黄达明,孙浩,曾庆凯[1]（2016）在《含有析取语义循环的不变式生成改进方法》一文中研究指出抽象解释为程序不变式的自动化生成提供了通用的框架,但是该框架下的大多数已有数值抽象域只能表达几何上是凸的约束集.因此,对于包含(所对应的约束集是非凸的)析取语义的特殊程序结构,采用传统数值抽象域会导致分析结果不精确.针对显式和隐式含有析取语义的循环结构,提出了基于循环分解和归纳推理的不变式生成改进方法,缓解了抽象解释分析中出现的语义损失问题.实验结果表明:相比已有方法,该方法能为这种包含析取语义的循环结构生成更加精确的不变式,并且有益于一些安全性质的推理.(本文来源于《软件学报》期刊2016年07期）
余伟[2]（2014）在《基于消元法生成非线性循环不变式》一文中研究指出本文基于消元法生成非线性循环不变式的相关算法。程序首先被转换成代数变迁系统,再根据其代数变迁关系和不变式模板构造一个多项式组,把不变式模板中适当变量通过消元法消去,则可以得到关于模板变量的约束关系,通过对该约束关系求解就得到循环不变式。经实例分析,该算法可广泛应用于线性、非线性循环不变式的生成。(本文来源于《电子技术与软件工程》期刊2014年16期）
余伟[3]（2014）在《循环不变式在程序设计教学中的应用》一文中研究指出本文介绍了循环不变式的理论和特点,在详细分析循环结构的基础上,结合实例介绍了在教学中引导学生通过循环不变式设计循环程序的过程,给出了通过循环不变式设计循环程序的具体步骤。(本文来源于《科技风》期刊2014年14期）
杨黄磊,薛锦云[4]（2014）在《一类单元赋值语句型循环不变式的开发方法研究》一文中研究指出依据现有循环不变式的定义和开发策略,阐述了一类单元赋值语句型循环不变式开发方法,同时使用Dijkstra最弱前置谓词方法确认了循环不变式的正确性.最后通过典型实例来说明该方法的应用.(本文来源于《江西师范大学学报(自然科学版)》期刊2014年04期）
杨黄磊[5]（2014）在《单元赋值语句型循环不变式的开发方法研究》一文中研究指出“软件危机”的出现，对于软件的可靠性和生产效率提出了更高的要求，形式化开发软件是一个很好的解决办法。而形式化开发软件就是要保证能对算法程序进行正确的推导和证明。而循环不变式是算法程序进行推导和证明的基石。任何一个循环程序都存在一个循环不变式，它在循环执行前和每次迭代后都能成立，当达到循环退出条件时，它产生了循环的最后结果。然而循环不变式无论是手工开发，还是自动构造一直都是一个巨大的挑战。本团队承担了国家自然科学基金重大国际合作项目：若干软件新技术及其在PAR平台中的实验研究。其中研究方向之一就是循环不变式的构造和自动探测。本文首先分析了国内外对循环不变式的定义及其开发方法的研究现状。然后介绍了本团队基于问题求解序列递推关系的循环不变式开发方法。接着介绍单元赋值语句型循环不变式的开发方法：按照PAR方法中的循环不变式开发策略，首先开发出抽象的单元赋值语句型循环程序的循环不变式，即抽象的单元赋值语句型循环不变式，并用Dijkstra最弱前置谓词方法进行了形式化的证明，然后对于具体的单元赋值语句型循环程序，将其对应的抽象的单元赋值语句型循环不变式进行参数实例化即可得到所需的单元赋值语句型循环不变式。最后在本研究团队已有循环不变式自动生成系统中实现了单元赋值语句型循环不变式的自动生成。本文的创新点有如下3个方面：1.对单元赋值语句和单元赋值语句型循环程序进行了抽象，使得该方法具有一定的普遍性和典型性。2.运用Dijkstra最弱前置谓词方法对开发出的抽象的单元赋值语句型循环不变式进行了形式化证明。3.在本研究团队已有的循环不变式自动生成系统上扩充实现了单元赋值语句型循环不变式的自动生成。(本文来源于《江西师范大学》期刊2014-06-01）
刘自恒,曾庆凯[6]（2013）在《一种自适应的循环不变式生成方法》一文中研究指出基于条件赋值转换和自适应模板生成技术,提出一种自适应的的循环不变式生成方法。该方法在生成过程中综合考虑函数规范、循环本身、循环后操作等信息,有针对性地发现潜在的循环不变式,并在Frama-C平台上实现一个插件loopInv。实验结果表明,与invGen和gin-pink工具相比,loopInv的应用更加有效,可较好地完成多数程序的验证过程。(本文来源于《计算机工程》期刊2013年06期）
许欢,王以松[7]（2012）在《用daikon发现循环不变式》一文中研究指出随着软件行业的深入发展,软件存在的问题与日俱增,程序正确性受到了广泛的关注,形式化方法是解决程序正确性的基本途径,而发现程序循环不变式是证明程序正确性的关键。本文介绍了循环不变式的基本概念以及计算不变式的基本方法;用JAVA重写了Siemens的replace C程序,并以JAVA和C两种语言的replace程序为例,对不变式动态探测工具daikon进行了深入的实验研究,试验结果揭示了daikon在探测循环语句不变式方面的不足,依此提出了改进daikon探测循环不变式的措施。(本文来源于《贵州大学学报(自然科学版)》期刊2012年04期）
余伟,冯勇[8]（2012）在《用Dixon结式产生非线性循环不变式》一文中研究指出针对循环程序的部分正确性问题,在代数变迁系统理论基础上,结合约束理论提出了一种用Dixon结式生成循环不变式的算法。首先,程序被转换成代数变迁系统,再根据代数变迁关系和不变式模板构造一个多项式组,计算此多项式组的Dixon结式可以得到关于模板变量的约束,最后对该约束系统求解就得到该模板形式的程序不变式。经实例分析,该算法应用于单路径和多路径程序均是有效的。(本文来源于《四川大学学报(工程科学版)》期刊2012年04期）
刘自恒[9]（2012）在《循环不变式生成方法研究与改进》一文中研究指出软件作为信息系统的实现载体,广泛应用在各个领域,软件中的任何安全漏洞或错误的实现都可能导致非常严重的后果。通过大量的测试可以提高软件的可靠性,但成本较高,也不能完全保证软件的可靠。形式化证明方法基于严密的数学和逻辑基础,经过正确性证明的程序可以保证软件符合指定的程序规范,从而大大提高软件可靠性。程序正确性证明的一个关键问题是发现充分的循环不变式信息来辅助、支撑证明过程的完成。由人工寻找循环不变式工作繁琐,容易出错。因此,研究如何自动地有效分析和生成循环不变式,使得软件证明过程顺利完成,成为形式化方法研究领域的一个重要研究课题。本文主要针对软件验证技术中的循环不变式生成技术进行研究和实现：(1)对形式化程序分析方法主要理论进行总结。本文根据形式化分析中用到的主要理论的不同对形式化分析技术进行总结。对各自的理论核心、主要解决的问题、典型工具进行了阐述。在此基础上,指出形式化证明过程的难点,并总结了当前克服这些难点所采用的方法。(2)介绍和总结了目前求解循环不变式的主要研究状况和现有方法。根据他们主要理论和适用范围的不同进行阐述,指出了目前工作存在的不足。(3)本文提出了一种基于条件赋值转换和自适应模板技术的循环不变式生成方法。根据程序控制流结构、依赖分析结果和值分析结果,生成可能的循环不变式,然后由定理证明器求解。该方法可以自动地运行,并将结果以ACSL注释的形式添加到程序中,辅助完成程序属性的证明过程。(4)基于上述方法,在Frama-C平台和APRON库的基础上,实现了一个分析插件loopInv。选取了一些程序作为分析对象,与其他方法作了比较,结果表明可以发现更多的不变式,使一些程序规范顺利得到证明。(本文来源于《南京大学》期刊2012-05-01）
邢建英,李梦君,李舟军[10]（2012）在《基于不变式生成的循环停机性验证》一文中研究指出循环的停机性验证是程序验证中的一个难点。程序不变式用来描述程序变量的取值关系,其中线性不变式可以帮助描述程序变量间的线性关系,循环不变式能够有效刻画循环中的变量关系。本文基于线性不变式和多项式循环不变式的生成,将循环的停机性验证转化为求解一个最优化问题,给出了一个实用的程序停机性验证框架。基于该框架可以自动地验证程序的停机性,并给出循环的复杂度上界。实验结果说明了该方法的实用性。(本文来源于《计算机工程与科学》期刊2012年04期）
循环不变式论文开题报告
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
本文基于消元法生成非线性循环不变式的相关算法。程序首先被转换成代数变迁系统,再根据其代数变迁关系和不变式模板构造一个多项式组,把不变式模板中适当变量通过消元法消去,则可以得到关于模板变量的约束关系,通过对该约束关系求解就得到循环不变式。经实例分析,该算法可广泛应用于线性、非线性循环不变式的生成。
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
循环不变式论文参考文献
[1].潘建东,陈立前,黄达明,孙浩,曾庆凯.含有析取语义循环的不变式生成改进方法[J].软件学报.2016
[2].余伟.基于消元法生成非线性循环不变式[J].电子技术与软件工程.2014
[3].余伟.循环不变式在程序设计教学中的应用[J].科技风.2014
[4].杨黄磊,薛锦云.一类单元赋值语句型循环不变式的开发方法研究[J].江西师范大学学报(自然科学版).2014
[5].杨黄磊.单元赋值语句型循环不变式的开发方法研究[D].江西师范大学.2014
[6].刘自恒,曾庆凯.一种自适应的循环不变式生成方法[J].计算机工程.2013
[7].许欢,王以松.用daikon发现循环不变式[J].贵州大学学报(自然科学版).2012
[8].余伟,冯勇.用Dixon结式产生非线性循环不变式[J].四川大学学报(工程科学版).2012
[9].刘自恒.循环不变式生成方法研究与改进[D].南京大学.2012
[10].邢建英,李梦君,李舟军.基于不变式生成的循环停机性验证[J].计算机工程与科学.2012