软件学报

作者：杜一德，洪伟疆，陈振邦，王戟

单位：杜一德，国防科技大学 计算机学院, 湖南 长沙 41007311,洪伟疆，国防科技大学 计算机学院, 湖南 长沙 410073;高性能计算国家重点实验室(国防科技大学), 湖南 长沙 41007302,陈振邦，国防科技大学 计算机学院, 湖南 长沙 41007303,王戟，国防科技大学 计算机学院, 湖南 长沙 410073;高性能计算国家重点实验室(国防科技大学), 湖南 长沙 41007304

关键词：合作验证;未解释程序;反例抽象精化;路径抽象;复用

基金：国家自然科学基金（62172429，62032024）

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

来源：2023年第7期

《软件学报》期刊编辑部

查看软件学报杂志2023年第7期