Automatic proving or disproving equality loop invariants based on finite difference techniques

•Equality loop invariants are characterized by finite difference techniques.•Equality loop invariants are proved or disproved by finite difference techniques.•The effectiveness is demonstrated with the experimental results.

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.