**This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.**

### Abstract

The magic wand $\mathbin{-\!\!*}$ (also called separating
implication) is a separation logic connective commonly used to specify
properties of partial data structures, for instance during iterative
traversals. A

*footprint*of a magic wand formula $$A \mathbin{-\!\!*} B$$ is a state that, combined with any state in which $A$ holds, yields a state in which $B$ holds. The key challenge of proving a magic wand (also called*packaging*a wand) is to find such a footprint. Existing package algorithms either have a high annotation overhead or are unsound. In this entry, we formally define a framework for the sound automation of magic wands, described in an upcoming paper at CAV 2022, and prove that it is sound and complete. This framework, called the*package logic*, precisely characterises a wide design space of possible package algorithms applicable to a large class of separation logics.