Permission-based veri fication logics such as separation logic have led to the development of many practical veri fication tools over the last decade. Verifi ers employ the separating conjunction A ‡* B to elegantly handle aliasing problems, framing, race conditions, etc. Introduced along with the separating conjunction, the magic wand connective, written A –* B, can describe hypothetical modi fications of the current state, and provide guarantees about the results. Its formal semantics involves quantifying over states: as such, the connective is typically not supported in automatic verifi cation tools. Nonetheless, the magic wand has been shown to be useful in by-hand and mechanised proofs, for example, for specifying loop invariants and partial data structures.

In this paper, we show how to integrate support for the magic wand into an automatic verifi er, requiring low specifi cation overhead from the tool user, due to a novel approach for choosing footprints for magic wand formulas automatically. We show how to extend this technique to interact elegantly with common specifi cation features such as recursive predicates. Our solution is designed to be compatible with a variety of logics and underlying implementation techniques.

We have implemented our approach, and a prototype veri fier is available to download, along with a collection of examples.