Reasoning in The Bernays-Schonfinkel-Ramsey Fragment of Separation Logic (VMCAI 2016 submission)

Andrew Reynolds, Radu Iosif, Cristina Serban.

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: 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 manually instantiated benchmarks from our paper can be found here: manual.tgz. To run CVC4 on these benchmarks, you simply run the binary with no command line arguments.
• The automatically instantiated benchmarks from our paper can be found here: nmanual.tgz. To run CVC4 on these benchmarks, use the command line arguments: --quant-epr --finite-model-find --no-quant-split.