Automated Program Verification Using Generation of Invariants

Program verification based on invariant generation is a central issue in recent years. Invariants are key to deductive verification of imperative programs. In this paper, depending on linear invariants and polynomial loop invariants, we present a practical program verification framework. The safety property and the termination property can be verified automatically. The experimental results demonstrate the power of our approach.