Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
Separation Logic S is a well-known assertion language used in Hoare-style modular proof systems for programs with dynamically allocated data structures. In this paper we investigate the fragment of first-order S restricted to the Bernays-Schönfinkel-Ramsey quantifier prefix ∃∀, where the quantified variables range over the set of memory locations. When this set is uninterpreted (has no associated theory) the fragment is PSPACE-complete, which matches the complexity of the quantifier-free fragment. However, S becomes undecidable when the quantifier prefix belongs to ∃∀∃* instead, or when the memory locations are interpreted as integers with linear arithmetic constraints, thus setting a sharp boundary for decidability within S. We have implemented a decision procedure for the decidable fragment of ∃∀S as a specialized solver inside a DPLL(T) architecture, within the CVC4 SMT solver. The evaluation of our implementation was carried out using two sets of verification conditions, produced 1) unfolding inductive predicates, and 2) weakest precondition-based verification condition generator. Experimental data shows that automated quantifier instantiation has little overhead, compared to manual model-based instantiation.
Sun 15 Jan
|16:00 - 16:30|
Ernst Moritz HahnState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Sven ScheweUniversity of Liverpool, Andrea TurriniState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun ZhangInstitute of Software, Chinese Academy of SciencesFile Attached
|16:30 - 17:00|
Andrew ReynoldsEPFL, Radu IosifVERIMAG, CNRS, Université Grenoble-Alpes, Cristina SerbanVERIMAG, CNRS, Université Grenoble-AlpesFile Attached
|17:00 - 17:30|