A Decision Procedure for Separation Logic in SMT (ATVA 2016)

Andrew Reynolds, Radu Iosif, Cristina Serban, Tim King.

We provide the following supplementary material for our paper.

Solver

The .tgz containing the binary of CVC4 used in our experiments can be downloaded here: sl-cvc4.tgz.

Source Code

The source code for CVC4 with support for separation logic has now been incorporated into the CVC4 master source.

Benchmarks

The benchmarks we consider in the paper can be found here: examples.tgz. The rows of Table 1 (8 below "Unfoldings of Inductive Predicates" and 8 below "Verification Conditions") correspond to following benchmarks, where the column is the number n in "[row name]-n.smt2":

• Unfoldings of Inductive Predicates - sorted-lists, trees, unfold-sat, unfold-unsat, nested-sat, nested-unsat, chain-sat, chain-unsat
• Verification conditions - dispose, dispose-iter, test-dispose, test-dispose-iter, rev, rev-iter, test-rev, test-rev-iter