SL-COMP 2018

SL-COMP is an initiative for collecting decision problems in Separation Logic and solvers dealing with such problems.

This initiative started in 2014 and it was inspired by the very popular initiatives on other theories, like first-order theories for SMT-COMP and Boolean constraints for SAT.

• July 14: Results and their ADSL presentation are available online.
• July 13: To present your solver at ADSL 2018, please read the mailing list.
• July 10: provisional results
• July 8: first round of the competition
• June 25: Solver registration ended.
• June 18: New benchmarks have been added. Many thanks to contributors!
• May 23: Call for comments, solvers, and benchmarks issued.
• January 2018: Announcement of the second edition of SL-COMP: it will be hosted by ADSL workshop at FLOC'18 in July 13th 2018.

• July 8: first round of the competition
• July 11: last round of the competition
• July 13: presentation at ADSL 2018; all participants are welcome to present their solver!

Separation Logic (SL) is an established and fairly popular Hoare logic for the imperative, heap-manipulating programs.

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 dynamic memory and whose properties are specified using SL.

These tools intensively use (semi-)decision procedures for checking satisfiability and entailment problems in SL. In the last ten 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 Separation Logic problems. This competition was inspired by the very popular competitions on other logic theories, e.g., SMT-COMP and SAT. This first edition of SL-COMP has been held with the support of the StarExec platform and of SMT-COMP officers, mainly David Cok.

The input format of problems extended the format SMT-LIB with SL constructs. This format has been changed for the second edition of SL-COMP in 2018 to better exploit the new features of SMT-LIB like datatypes definition and mutually recursive functions.

The input problems are specified using the format described here and commented in this post.

Problems to be solved are either satisfiability problems or entailment problems. An entailment problem consists in checking the validity of the formula \(A \models B\) and it is coded by the formula \(A \land \lnot B\).

The possible answers of a solver are: sat, unsat, unknown.

The solvers shall run on the StarExec platform. Solvers may use a pre-processor to transform the input file format to the solver's format. The input problems are not scrambled.

• SL-COMP 2018 collected a set of 1296 problems. This set includes the one in the 2014 edition (678 problems, see below) and new problems. The current set of problems is split into the following divisions:
  • Satisfiability checking:
    • qf_shls_sat: for quantifier free (QF) formulas in the symbolic heaps (SH) fragment using only acyclic singly linked lists
    • qf_shid_sat: for QF formulas in the SH fragment using general inductive definitions (ID)
    • qf_shidlia_sat: for QF formulas in the SH fragment with ID and linear integer constraints (LIA)
    • qf_bsl_sat: for QF fragment with boolean combination of SL atoms; the quantified version of this division bsl_sat has not enough problems to be considered by this edition
    • qf_bsllia_sat: for QF fragment with boolean combination of SL atoms and LIA
  • Entailment checking:
    • qf_shls_entl: for QF formulas in the SH fragment using only acyclic singly linked lists
    • qf_shid_entl: for QF formulas in the SH fragment with ID
    • qf_shlid_entl: for QF formulas in the SH fragment with linear ID
    • shid_entl: for formulas in the SH fragment with ID
    • qf_shidlia_entl: for formulas in the SH fragment with ID and LIA
    • shidlia_entl: for QF formulas in the SH fragment with IS and LIA
• SL-COMP 2014 collected a set of 678 problems with the following properties:
  • 25% satisfiability problems versus 75% entailment problems
  • 41% crafted problems versus 59% random generated problems
  • The problems were split in four divisions:
    • sll0a_sat: satisfiability problems for the SH fragment with a unique inductive definition (ID) specifying acyclic singly linked list
    • sll0a_entl: entailment problems for the above fragment
    • FDB_entl: entailment problems for the SH fragment with linear ID specifying various kinds of lists in a restricted way
    • UDB_sat: satisfiability problems for the SH fragment with general, user defined ID specifying lists, trees, etc
    • UDB_entl: entailment problems for the above fragment
• The contributions to the benchmark of SL-COMP are summarized below:

These are the solvers participating in the SL-COMP 2018.

These are the benchmark divisions in which each solver is competing:

The list of participants at SL-COMP 2014 is provided here.

• The StarExec configuration is fixed to:
  • before July 9th: 120 sec of timeout and 1 GB of memory.
  • after July 9th: 600 sec of timeout and 4 GB of memory.
• Several rounds are run between July 8th and July 11th.
• The final results will be announced July 13th, 2018, at the ADSL workshop, presentation is available on GitHub repository.
• Overview of results for each division is provided below.

The organisation committee of SL-COMP 2018 includes the organisers of the ADSL workshop, namely Nikos Gorogiannis, Radu Iosif and Mihaela Sighireanu.

The competition committee will include a member for each participating solver.

Any question related to this competition shall be sent to the organisation committee and to the mailing list.

• SL-COMP 2014