Towards Automatic Deductive Verification of C Programs over Linear Arrays

Abstract

The generation and proving of verification conditions, which correspond to loops, may cause difficulties during deductive verification because the construction of required invariants is a challenge, especially for nested loops. The methods of invariant synthesis are often heuristic ones. Another way is the symbolic method of loop invariant elimination. Its idea is to represent a loop body in a form of special replacement operation under certain constraints. This operation expresses loop effect with possible break statement in a symbolic form and allows introducing an inference rule, which uses no invariants in axiomatic semantics. This work represents the further development of this method. The inner loops are interesting because of the higher nesting level, the more complicated loop invariant. A good example for this case to verify is a class of linear array sorting programs, which iteratively increase the sorted part. In this paper, we consider the insertion sort program. A special algorithm was developed and implemented to prove verification conditions automatically in ACL2. It generates automatically auxiliary lemmas, which allow to prove obtained verification conditions in ACL2 in automatic mode.