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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:30
Decision proceduresVMCAI at Amphitheater 44
Chair(s): Andreas Podelski University of Freiburg, Germany
16:00
30m
Talk
Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games
VMCAI
Ernst Moritz Hahn State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Sven Schewe University of Liverpool, Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun Zhang Institute of Software, Chinese Academy of Sciences
File Attached
16:30
30m
Talk
Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
VMCAI
Andrew Reynolds EPFL, Radu Iosif VERIMAG, CNRS, Université Grenoble-Alpes, Cristina Serban VERIMAG, CNRS, Université Grenoble-Alpes
File Attached
17:00
30m
Talk
Matching multiplications in Bit-Vector formulas
VMCAI
Supratik Chakraborty IIT Bombay, Ashutosh Gupta , Rahul Jain Tata Institute of Fundamental Research
File Attached