Write a Blog >>
VMCAI 2017
Sun 15 - Tue 17 January 2017
co-located with POPL 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

Sun 15 Jan

16:00 - 17:30: VMCAI - Decision procedures at Amphitheater 44
Chair(s): Andreas PodelskiUniversity of Freiburg, Germany
VMCAI-2017-papers148449240000016: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 Sciences
File Attached
VMCAI-2017-papers148449420000016:30 - 17:00
Andrew ReynoldsEPFL, Radu IosifVERIMAG, CNRS, Université Grenoble-Alpes, Cristina SerbanVERIMAG, CNRS, Université Grenoble-Alpes
File Attached
VMCAI-2017-papers148449600000017:00 - 17:30
Supratik ChakrabortyIIT Bombay, Ashutosh Gupta, Rahul JainTata Institute of Fundamental Research
File Attached