摘要

Loop invariants play a major role in software verification. In this paper, based on finite difference techniques, a formal characterization for equality loop invariants is presented. Integrating the formal characterization with the automatic verification approach in [5], the algorithm for automatic proving or disproving equality loop invariants is presented. The effectiveness of the algorithm is demonstrated with the experimental results.