Trace Abstraction-Based Verification for Uninterpreted Programs

The verification of uninterpreted programs is undecidable in general. This paper proposes to employ counterexample-guided abstraction refinement (CEGAR) framework for verifying uninterpreted programs. Different from the existing interpolant-based trace abstraction, we propose a congruence-based trace abstraction method for infeasible counterexample paths to refine the program’s abstraction model, which is designed specifically for uninterpreted programs. Besides, we propose an optimization method that utilizes the decidable verification result for coherent uninterpreted programs to improve the CEGAR framework’s efficiency. We have implemented our verification method and evaluated it on two kinds of benchmark programs. Compared with the state-of-the-art, our method is more effective and efficient, and achieves 3.6x speedups on average.