Reasoning in the Bernays-Schoenfinkel-Ramsey Fragment of Separation Logic

Andrew Reynolds, Radu Iosif, Cristina Serban

Separation Logic (SL) is a well-known assertion language used in Hoare-style modular proof systems for programs with dynamically allocated data structures. In this paper we investi…