Post-condition-Directed Invariant Inference for Loops over Data Structures

In the automatic code verification, it is often necessary for programmers to provide logical annotations in the form of pre-/post-conditions and loop invariants. In this paper, we propose a framework that automatically infers loop invariants of loops manipulating commonly-used data structures. These data structures include one-dimensional arrays, singly-linked lists, doubly-linked lists and static lists. In practical cases, a majority of the loops operating on such data structures work by iterating over the elements of these data structures. The loop invariants of this kind of loops are usually similar in form with their corresponding post-conditions. The framework takes advantage of this observation by generating invariant candidates automatically from a given post-condition following several heuristics. These invariant candidates are subsequently validated via the SMT solver Z3 and the weakest-precondition calculator provided in the interactive code-verification tool Accumulator. The framework, which has been implemented for a small C-like language, suffices to infer suitable loop invariants of a range of loops w.r.t. given post-conditions. The framework has been integrated into the tool Accumulator to ease the verification tasks by alleviating the burden of providing loop invariants manually.