Email Gateway (May 27 2022 at 14:02): Email Gateway (May 27 2022 at 14:02):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce a new entry, by Thibault Dardinier:
Formalization of a Framework for the Sound Automation of Magic Wands
The magic wand (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-*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.
It is online at https://www.isa-afp.org/entries/Package_logic.html
Larry
Last updated: Jul 15 2022 at 23:21 UTC