程序验证相关论文
实时系统、嵌入式系统等反应式系统（Reactive Systems）往往具有“同步”特性,即模块间通信时间可忽略不计,同一时刻多个信号可同时发......
“万物互联”概念的提出,推动着智慧城市与智能家居等各个智能场景下科技的发展,多场景应用无缝体验成为智慧生活的基石。智能设备......
随着软件规模和复杂度的不断提高,软件缺陷问题不断出现。如何提高软件的可靠性已经成为软件工程领域的一个重要研究问题。程序验......
在交互式的程序验证中,人们希望自动化地获得一些信息来提高证明效率。数据流分析是一类典型的静态程序分析方法。将这些分析方法......
随着软件技术的发展，程序的规模逐渐增大，复杂度也逐渐增加。在软件的开发过程中，完全依靠人力进行分析测试效率太低，而且不能保证软件......
计算机软硬件技术的快速发展，使得软件的应用渗透到了社会的各个领域，从手机到internet，软件在人们的生活中扮演着重要的角色。然而，随......
本文综合叙述了已有的基于程序语言设计的软件安全研究。按照对安全性质推理方法的不同，将这类研究分成基于Hoare逻辑和基于类......
随着Internet的广泛应用和移动计算领域的不断扩大，人们对高可信软件的需求越来越多，从而对软件的可靠性和安全性提出了更高的挑战，因......
现今计算机和互联网技术的迅速发展不仅带来了具有更强计算能力的计算机、更加便捷的信息交流方式，而且也对计算机软件的安全性和可......
随着软件逐渐被应用到国家、社会的更广、更深的领域中，随之而来的软件安全性问题也不容忽视。重要领域、行业的关键软件的安全性问......
BPEL作为描述Web服务编制的语言之一,在商业流程中被用来描述活动和对活动的控制。BPEL具有类似程序设计语言的语法结构,如顺序、......
随着计算机硬件平台运算能力的不断提升，计算机软件的规模及复杂度日益增长，同时软件安全性问题也日益突出。如何解决软件安全性，已然......
随着计算机应用的日益推广,我们对软件的可靠性和安全性的需求越来越高。这些需求体现在安全攸关的基础设施和系统上,包括核电、航......
随着计算机科学的迅速发展,软件规模日益庞大。现在人们在考虑软件执行效率的同时,也越来越关注其安全性(Safety)。高可信软件的研......
随着计算机科学技术的飞速发展,计算机软件的规模日益庞大,调试和维护越来越困难。而另一方面,软件的安全形势严峻,对未受信源提供......
从上世纪六十年代起,随着大型软件的快速发展,人们对软件质量的要求起来越高,尤其是对软件的正确性要求。计算机界为确保软件质量......
Web服务编排描述语言(Web Services Choreography Description Language,简称WS-CDL)从全局的视点描述服务组合各个参与方的行为规......
随着计算机软件在社会各行各业的广泛应用,程序安全成为人们越来越关注的问题。尤其是当大量计算机软件被用于航空航天、武器、大......
循环程序的终止性分析是程序验证的重要组成部分。确保循环程序的终止是循环程序完全正确的必要条件。目前,用来证明程序终止性的......
模型检测是一种形式化验证技术,主要用于系统的建模和分析。随着软件系统规模和复杂性的增加,模型检测中的状态爆炸问题愈发严重。......
学位
工业控制系统的正确可靠对经济发展、人身安全和社会稳定有着重要意义。工业控制系统面对的一个基本问题是控制中的时序问题。如何......
OSEK/VDX作为分布式实时系统的标准,已被汽车电子行业广泛采用。为提高汽车的整体性能,应用程序的设计趋于并行和复杂化,OSEK/VDX......
本文基于组合导航接收机的研制背景,对在VB环境中开发上位机软件进行了详细的说明,其中包括上位机与下位机之间的数据通信、数据的......
随着计算机硬件平台运算能力的不断提升，计算机软件的规模及复杂度日益增长，同时软件安全性问题也日益突出。如何解决软件安全性，已然......
本文对2243VMC立式加工中心仿真系统进行了研究。文章在充分了解2243VMC立式加工中心结构、性能、编程语言及加工过程的基础上，在计......
本文论述了反编译作为一种程序验证的工具在航天工业中的重要地位和应用；介绍了反编译的背景知识；给出一个实用的反编译系统ＤＣＰＬ的设计模......
携带证明代码允许代码消费方通过检查代码生产方提供的证明,来判断代码是否满足相应的安全规范.本文实现了一个类C语言的出具证明......
在一个类C小语言PointerC的程序验证器原型的实现中,设计并实现了对一维数组元素进行赋值的语句的推理规则.该推理规则是Hoare逻辑......
在一个基于形状图逻辑的C语言程序自动验证系统上,设计并实现了二叉树形状程序的循环不变形状图的自动推断方法.该方法与单链表程......
期刊
针对柱对称二维流体力学方程组,基于考虑方程右端附加源项的人为构造解方法,构造出一类统一形式的人为解.此类形式的人为解,对验证......
本文较详细地叙述了先进压水堆铁-水反射层组件研制及实验研究的主要内容和实验结果,并利用实验结果对计算程序进行了验证和分析。......
基于逻辑推理的方法进行程序验证是形式化程序验证的研究热点.目前的自动验证工具为了保证自动性,对描述程序性质的断言语言都有较......
近来在程序验证领域,Feng和Shao提出一个类Hoare逻辑的验证框架以验证包含中断的底层程序.在该工作基础上进行扩展,提出一个验证包......
期刊
在指针程序的分析和验证过程中,循环不变式的自动推断一直是个研究热点.文章首先介绍所提出的形状图和形状图逻辑,形状图逻辑是一......
全球安全身份信息解决方案的领导者HID Global日前宣布，推出一款基于云的新平台，以帮助部署安全的近距离无线通信（Near Field Communi......
在并发程序的分析及验证过程中,不变式起着至关重要的作用,为了提高非线性不变式自动生成算法的效率及通用性,基于将非线性不变式......
Yogar-CBMC基于事件顺序图实现了反例抽象精化思想,是当前最有效的多线程程序验证工具之一。针对事件顺序图过于复杂,导致判断反例......
随着计算机系统复杂性的日渐增加,可靠性正成为计算机软件理论中新的研究热点.运用数理逻辑中的推理方法,研究人员可以严格分析和......
程序安全性验证是程序验证的重要部分。基于不变式生成,将程序的安全性验证转化为验证不变式集合是否蕴含表示安全性的逻辑公式。......
提出一类非线性循环程序的终止性是可以判定的。该类程序的终止性与其赋值矩阵的正特征值相对应的特征向量有关。然后提出了一种新......
针对形式化程序验证中的并行调度问题，提出了基于依赖集的算法。通过引入依赖图和依赖集概念，以形式化方式描述程序语句间的依赖关系......
面向新工科背景和建设中对人才的需求,针对模型检测与程序验证课程传统教学中教学模式单一、理论与实践融合度低等问题,提出将理论......
介绍了分离逻辑的验证原理和特点及其在程序验证方面的应用实例，分析了为支持程序验证的若干分离逻辑研究进展，包括分离逻辑的自身属......
由于多栈的模型图灵等价,因此,通用的异步通信程序模型的验证问题不可判定.为此,基于Petri网,提出了一个新的模型通信——通信Petr......
类型系统能检出合法程序的语义错误，可以缩短调试时间，在执行程序之前捕获代码中的错误。类型系统的理论基础是类型化的λ演算。带子......
作为一种通用的语义近似理论，抽象解释已广泛应用于各类程序的形式化验证中。现有基于抽象解释的逻辑程序验证技术未涉及与程序点相......
