Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution

Peter Müller, Malte Schwerhoff, Alexander J. Summers

In permission logics such as separation logic, the iterated separating conjunction is a quantifier denoting access permission to an unbounded set of heap locations. In contrast to…