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.