POPL 2017
Sun 15 - Sat 21 January 2017
Sun 15 Jan 2017 16:30 - 17:00 at Amphitheater 44 - Decision procedures Chair(s): Andreas Podelski

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.

slides (vmcai17-serban.pdf)455KiB