| 摘要: |
| 未解释程序的验证问题通常是不可判定的，但是最近有研究发现，存在一类满足coherence性质的未解释程序，其验证问题是可判定的，并且计算复杂度为PSPACE完全的.在此结果的基础上，一个针对一般未解释程序验证的基于路径抽象的反例抽象精化（counterexample-guided abstraction refinement，CEGAR）框架被提出，并展现了良好的验证效率.即使如此，对未解释程序的验证工作依然需要多次迭代，特别是利用该方法在针对多个程序验证时，不同的程序之间的验证过程是彼此独立的，存在验证开销巨大的问题.发现被验证的程序之间较为相似时，不可行路径的抽象模型可以在不同的程序之间复用.因此，提出了一个合作验证的框架，收集在验证过程中不可行路径的抽象模型，并在对新程序进行验证时，用已保存的抽象模型对程序进行精化，提前删减一些已验证的程序路径，从而提高验证效率.此外，通过对验证过程中的状态信息进行精简，对现有的基于状态等价的路径抽象方法进行优化，以进一步提升其泛化能力.对合作验证的框架以及路径抽象的优化方法进行了实现，并在两个具有代表性的程序集上分别取得了2.70x和1.49x的加速. |
| 关键词: 合作验证 未解释程序 反例抽象精化 路径抽象 复用 |
| DOI：10.13328/j.cnki.jos.006860 |
| 分类号: |
| 基金项目:国家自然科学基金（62172429，62032024） |
|
| Collaborative Verification Method of Uninterpreted Programs |
|
DU Yi-De1, HONG Wei-Jiang1,2, CHEN Zhen-Bang1, WANG Ji1,2
|
|
1.College of Computer Science and Technology, National University of Defense Technology, Changsha 410073, China;2.State Key Laboratory of High Performance Computing (National University of Defense Technology), Changsha 410073, China
|
| Abstract: |
| The verification of an uninterpreted program is undecidable in general. Recently, a decidable fragment (called coherent) of uninterpreted programs is discovered and the verification of coherent uninterpreted programs is PSPACE complete. Based on the results of coherent uninterpreted programs, a trace abstraction-based verification method in CEGAR (counterexample-guided abstraction refinement) style is proposed for general uninterpreted programs, and is very effective. Although that, the verification of uninterpreted programs sometimes needs many refinements. Especially when verify multiple programs with this method, the verifications of different programs are independent of each other and has high complexity. However, it is observed that those abstract models of infeasible counter-example traces are reusable and can benefit from each other’s verification when the programs to be verified are similar. In this work, a collaborative verification framework is proposed that accumulates the abstract models of infeasible traces during the programs’ verification. When a new program is to be verified, the program abstraction is refined with the accumulated abstract model first to wipe off those infeasible traces to improve the verification efficiency. Besides, an optimized congruence-based trace abstraction method is also proposed that compacting the states during the verification to enlarge the scope of the abstractions of the infeasible traces. The collaborative verification framework and the optimized trace abstraction method have been implemented, achieving on average 2.70x and 1.49x speedups on two representative benchmarks. |
| Key words: collaborative verification uninterpreted program counterexample-guided abstraction refinement trace abstraction reuse |
