Program verifiers based on separation logic, such as Gillian, VeriFast, and Viper, allow one to prove complex properties of heap-manipulating, concurrent programs. These tools automate a large part of the proof search, but require a substantial amount of annotations such as method pre- and postconditions and loop invariants. Inference techniques such as bi-abduction can alleviate this burden, but existing techniques are too restrictive to be used in expressive program verifiers. In particular, existing bi-abduction techniques do not support the magic wand connective, so that inference for iterative traversals of structures beyond list segments is limited. Moreover, they rely on an equirecursive interpretation of predicates, instead of the isorecursive interpretation used by most SMT-based verifiers.

In this paper, we present a novel abductive inference that addresses these limitations. It infers loop invariants that combine user-defined predicates with magic wands to keep track of the part of a data structure still to be traversed and the remainder of the data structure, such that ownership of the entire structure is retained after the traversal. Moreover, our abduction technique is the first to infer the auxiliary operations required by verifiers to manipulate predicates and wands.

We implemented our inference in Viper; our evaluation shows that our approach can infer over 80% of the specifications required to verify memory safety of a diverse benchmark set.