Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions

Neta Elad, Adithya Murali, Sharon Shoham

For over two decades Separation Logic has been arguably the most popular framework for reasoning about heap-manipulating programs, as well as reasoning about shared resources and p…