SL-COMP 2018
Table of Contents
- Synopsis
- News
- Key Dates
- Introduction
- Specifications and rules
- Benchmarks and divisions
- Participants
- Results
- Division
qf_bsl_sat
: 46 problems, 2 solvers - Division
qf_bsllia_sat
: 24 problems, 2 solvers - Division
qf_shid_entl
: 311 problems, 6 solvers - Division
qf_shid_sat
: 99 problems, 6 solvers - Division
qf_shidlia_entl
: 61 problems, 4 solvers - Division
qf_shidlia_sat
: 33 problems, 4 solvers - Division
qf_shlid_entl
: 59 problems, 7 solvers - Division
qf_shls_entl
: 296 problems, 8 solvers - Division
qf_shls_sat
: 110 problems, 8 solvers - Division
shid_entl
: 73 problems, 5 solvers - Division
shidlia_entl
: 181 problems, 3 solvers
- Division
- Committee
- Mailing list
- Previous SL-COMPs
Synopsis
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.
News
- 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.
Key Dates
- 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!
Introduction
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.
Specifications and rules
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.
Benchmarks and divisions
- 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 listsqf_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 divisionbsl_sat
has not enough problems to be considered by this editionqf_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 listsqf_shid_entl
: for QF formulas in the SH fragment with IDqf_shlid_entl
: for QF formulas in the SH fragment with linear IDshid_entl
: for formulas in the SH fragment with IDqf_shidlia_entl
: for formulas in the SH fragment with ID and LIAshidlia_entl
: for QF formulas in the SH fragment with IS and LIA
- Satisfiability checking:
- 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 listsll0a_entl
: entailment problems for the above fragmentFDB_entl
: entailment problems for the SH fragment with linear ID specifying various kinds of lists in a restricted wayUDB_sat
: satisfiability problems for the SH fragment with general, user defined ID specifying lists, trees, etcUDB_entl
: entailment problems for the above fragment
- The contributions to the benchmark of SL-COMP are summarized below:
Division | #problems | Asterix | ComSPEN | CVC4 | Cyclist | Harrsh | S2S | Sleek | Slide | Songbird | SPEN |
---|---|---|---|---|---|---|---|---|---|---|---|
qf_bsl_sat |
45 | 0 | 0 | 46 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
qf_bsllia_sat |
24 | 0 | 0 | 24 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
qf_shid_entl |
311 | 1 | 0 | 0 | 22 | 0 | 59 | 81 | 17 | 132 | 46 |
qf_shid_sat |
99 | 0 | 0 | 0 | 61 | 29 | 9 | 0 | 0 | 0 | 0 |
qf_shidlia_entl |
61 | 0 | 22 | 0 | 0 | 0 | 0 | 0 | 0 | 39 | 0 |
qf_shidlia_sat |
33 | 0 | 20 | 0 | 0 | 0 | 13 | 0 | 0 | 0 | 0 |
qf_shlid_entl |
59 | 0 | 0 | 0 | 0 | 0 | 13 | 0 | 0 | 0 | 46 |
qf_shls_entl |
296 | 287 | 0 | 0 | 0 | 0 | 9 | 0 | 0 | 0 | 5 |
qf_shls_sat |
110 | 110 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
shid_entl |
73 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 9 | 64 | 0 |
shidlia_entl |
181 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 181 | 0 |
Participants
These are the solvers participating in the SL-COMP 2018.
Solver | Preliminary | Final | System description | Contact |
---|---|---|---|---|
version id | version id | for StarExec | ||
Asterix | 986 | 20618 | Asterix | Juan Antonio Navarro PĂ©rez |
ComSPEN | 20429 | 20631 (pull out) | ComSPEN | Chong Gao |
Cyclist-SL | 1136,1137 | 1136,1137 | Cyclist-SL | Nikos Gorogiannis |
CVC4 | 20439 | 20439 | CVC4-SL | Andrew Reynolds |
Harrsh | 20535 | 20573 | Harrsh | Jens Katelaan |
S2S | 20562 | 20643 | S2S | Le Quang Loc |
Sleek | 20432 | 20564 | Sleek | Benedict Lee |
Slide | 20428 | 20628 | Slide | Adam Rogalewicz |
Sloth | pull out | Sloth | Jens Katelaan | |
Songbird | 20552 | 20617 | Songbird | Ta Quang Trung |
SPEN | 20561 | 20561 | SPEN | Mihaela Sighireanu |
These are the benchmark divisions in which each solver is competing:
Division | #prob | Asterix | ComSPEN | CVC4 | Cyclist | Harrsh | S2S | Sleek | Slide | Sloth | Songbird | SPEN |
---|---|---|---|---|---|---|---|---|---|---|---|---|
qf_bsl_sat |
46 | X | O | |||||||||
qf_bsllia_sat |
24 | X | O | |||||||||
qf_shid_entl |
311 | X | X | X | X | X | X | |||||
qf_shid_sat |
99 | X | X | X | X | X | X | |||||
qf_shidlia_entl |
61 | O | X | X | X | |||||||
qf_shidlia_sat |
33 | O | X | X | X | |||||||
qf_shlid_entl |
59 | O | X | X | X | X | X | X | ||||
qf_shls_entl |
296 | X | O | X | X | X | X | O | X | X | ||
qf_shls_sat |
110 | X | O | X | X | X | X | O | X | X | ||
shid_entl |
73 | X | X | X | X | X | ||||||
shidlia_entl |
181 | X | X | X |
The list of participants at SL-COMP 2014 is provided here.
Results
- 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.
Division qf_shlid_entl
: 59 problems, 7 solvers
Division qf_shls_entl
: 296 problems, 8 solvers
Division qf_shls_sat
: 110 problems, 8 solvers
Committee
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.
Mailing list
Any question related to this competition shall be sent to the organisation committee and to the mailing list.