A practical loop invariant generation approach based on random testing, constraint solving and verification

Abstract

Loop invariants play a major role in software verification. Based on random testing, constraint solving and verification, this paper presents a practical approach for generating equality loop invariants. More importantly, we present a practical verification approach of loop invariant based on finite difference technique. This approach is efficient since the constraint system is linear equational system. The effectiveness of the approach is demonstrated on examples. © 2012 Springer-Verlag.