Lightweight support for magic wands in an automatic verifier

Abstract

Permission-based verication logics such as separation logic have led to the development of many practical verication tools over the last decade. Veriers 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 modications 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 verication tools. Nonetheless, the magic wand has been shown to be useful in by-hand and mechanised proofs, particularly for specifying loop invariants and partial data structures. In this paper, we show how to integrate support for the magic wand into an automatic verier, requiring low specication overhead from the tool user. We present additional features to make the magic wand interact elegantly with abstract predicates, abstraction functions and \old" expressions. Our solution is compatible with a variety of logics and underlying implementation techniques. Our approach is implemented, and a prototype is available to download.