Formalization of a Framework for the Sound Automation of Magic Wands

Thibault Dardinier 🌐

May 18, 2022

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.

License

BSD License

Topics

Session Package_logic