Effective Entailment Checking for Separation Logic with Inductive Definitions: Supplementary Material
This repository contains the supplementary material for our TACAS 2019 paper "Effective Entailment Checking for Separation Logic with Inductive Definitions."
All proofs and an extended experimental evaluation can be found in a separate appendix avaliable here.
The complete set of benchmarks used to evaluate Harrsh are available here. The linked archive contains all benchmarks used in the experimental evaluation of the paper and the appendix in Harrsh, Songbird and Slide input formats. Note that the results of our evaluation are in the appendix.