Sound Automation of Magic Wands (extended version)

Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks +2

The magic wand $-\ast$ (also called separating implication) is a separation logic connective commonly used to specify properties of partial data structures, for instance…