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.