Report on SL-COMP 2014

Abstract

A competition of solvers for Separation Logic was held in May 2014, as an unofficial satellite event of the FLoC Olympic Games. Six solvers participated in the competition; the success and performance of each solver was measured over an appropriate subset of a library of benchmarks accumulated for the purpose. The benchmarks consisted of satisfiability and entailment problems over formulas in the fragment of symbolic heaps with inductive definitions, which is the fragment of Separation Logic that is most used in program analysis and verification tools. We report in this paper on the competition rules, the participants, the results, the findings, and the future of this event.