Home Separation Logic Specs Tools Thanks
Separation Logic (SL) is an established and fairly popular Hoare logic for the imperative, heap-manipulating programs, introduced nearly fifteen years ago by John C. Reynolds. Its high expressivity, its ability to generate compact proofs, and its support for local reasoning motivated the development of tools for automatic reasoning about programs using SL. These tools intensively use (semi-)decision procedures for checking satisfiability and entailment problems in SL. In the last five years, several papers reported on the design and implementation of such solvers.
To improve the status of these solvers and to motivate the research in this area, we started in May 2014 a competition of solvers for (a fragment of) Separation Logic problems. This competition was inspired by the very popular competitions on other logic theories, e.g., SMT-COMP and SAT competitions.
This first edition of SL-COMP has been held with the support of the StarExec platform and the SMT-COMP officers.
Last modified: Thu Sep 25 18:05:53 CEST 2014