VASR-CBMC：基于变量子图的多线程程序验证

Yogar-CBMC基于事件顺序图实现了反例抽象精化思想,是当前最有效的多线程程序验证工具之一。针对事件顺序图过于复杂,导致判断反例可行性及求解精化约束耗时过长的问题,提出变量子图概念及基于变量子图的抽象精化方法,将全局事件顺序图分解为连通等价的变量子图集,基于变量子图执行反例验证与精化求解,从而有效缩小图的规模,提升验证效率。将该方法实现为VSAR-CBMC,实验证明相较于Yogar-CBMC验证时间平均缩短43%。     

基于CEGAR偏序化简的并行程序死锁检测

针对并发程序的模型检测存在大量的冗余交互和严重的状态空间爆炸问题,提出以迁移标记系统为建模语言计算Persistent Set并完成偏序化简的算法。将算法和CEGAR算法结合起来,实现对并发C程序的并行死锁检测。结果证明该算法在减缓状态空间爆炸和模型验证的效率方面较以往的算法有所提高。     

基于Verds的C语言子集的模型检测方法

针对现今软件使用逻辑错误的问题越来越多的出现,提出了对最流行最普遍的编程语言1语言子集的模型检测方法的研究．采用基于Verds工具的模型,运用C语言子集转化成Verds模型的算法,结合Verds工具和MAGIC工具实现模型检测．引入反例引导的抽象精化方法使模型检测解决状态爆炸的问题．     

Refining abstract interpretations

Abstract interpretation techniques prove properties of programs by computing abstract fixpoints. All such analyses suffer from the possibility of false errors. We present a dag-based abstraction refinement technique to automatically refine such abstract interpretations and reduce false errors. This technique refines precision loss due to widen operator by a new interpolated widen operator and refines precision loss due to join operator by disjunctions. We prove the soundness and progress properties of this abstraction refinement procedure.     

面向未解释程序的合作验证方法

未解释程序的验证问题通常是不可判定的,但是最近有研究发现,存在一类满足coherence性质的未解释程序,其验证问题是可判定的,并且计算复杂度为PSPACE完全的.在这个结果的基础上,一个针对一般未解释程序验证的基于路径抽象的反例抽象精化（CEGAR）框架被提出,并展现了良好的验证效率.即使如此,对未解释程序的验证工作依然需要多次迭代,特别是利用该方法在针对多个程序验证时,不同的程序之间的验证过程是彼此独立的,存在验证开销巨大的问题.本文发现被验证的程序之间较为相似时,不可行路径的抽象模型可以在不同的程序之间复用.因此,本文提出了一个合作验证的框架,收集在验证过程中不可行路径的抽象模型,并在对新程序进行验证时,用已保存的抽象模型对程序进行精化,提前删减一些已验证的程序路径,从而提高验证效率.此外,本文通过对验证过程中的状态信息进行精简,对现有的基于状态等价的路径抽象方法进行优化,以进一步提升其泛化能力.本文对合作验证的框架以及路径抽象的优化方法进行了实现,并在两个具有代表性的程序集上分别取得了2.70x和1.49x的加速.     

一种C程序断言的全自动静态验证方法

在软件程序中插入断言是保证软件质量的一个简单但有效的方法，人们常使用测试的方法检验程序中的断言是否满足，但测试很难保证验证的完备性。本文提出了一种可以保证完备性的全自动静态断言验证方法，其基本思想是基于程序切片符号执行程序的所有执行路径，并证明路径上的所有断言都满足。为了尽量减少符号执行的语句的数量，使用了基于反例的抽象精化方法，从一个粗略的切片标准开始迭代地符号执行一爷路径，根据验证的反例自动生成下一次迭代过程中使用的精化的切片标准。包含循环的程序可能具有无穷多条程序执行路径，提出的基于符号执行上下文不变式证明的方法可以证明由于循环导致的无穷多条路径中断言都满足，从而使得验证过程可以终止。实验表明，提出的全自动静态断言验证方法不仅可行，而且验证代价较小，具有较强的实用性。