SL-COMP 2019
Table of Contents
- Synopsis
- News and Key Dates
- Specifications and rules
- Benchmarks and divisions
- Participants
- Results
- Division
qf_bsl_sat
: 46 problems, 1 solver - Division
qf_bsllia_sat
: 24 problems, 1 solver - Division
qf_shid_entl
: 312 problems, 6 solvers - Division
qf_shid_sat
: 99 problems, 5 solvers - Division
qf_shidlia_entl
: 61 problems, 4 solvers - Division
qf_shidlia_sat
: 33 problems, 4 solvers - Division
qf_shlid_entl
: 60 problems, 8 solvers - Division
qf_shls_entl
: 296 problems, 9 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
Synopsis
This is the 3rd edition of SL-COMP, 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.
For more details, see competition's web site.
News and Key Dates
- April 6-7, 2019: Presentation of SL-COMP'19 at TOOLympics 2019
- March 31, 2019: Last official run of SL-COMP'19 on StarExec
- March 22, 2019: First official run of SL-COMP'19 on StarExec
- March 8, 2019: First training run of SL-COMP'19 on StarExec
- February 25, 2019: Preliminary description of SL-COMP'19 at TOOLympics 2019 available at competition's web site
- January 8, 2019: Deadline for registration of solvers for SL-COMP 2019 at easychair submission site
- December 7, 2018: Call for participation to SL-COMP 2019 at TOOLympics 2019
Specifications and rules
The same input format as for SL-COMP 2018 edition, detailed on competition web site.
The competition takes place on the StarExec platform based on the following rules:
- timeout for solving one problem: 2400 seconds except for division
qf_shls_*
whre timeout is 600 seconds - maximum memory: 10 GB
- no scrambling
- official pre-processors accepted
The scoring scheme used is explained here
Benchmarks and divisions
This edition uses the same set of problems than SL-COMP 2018 edition, i.e., 1296 problems split into the same 11 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
A set of new problems proposed for division `qfshidentl` are on probation at this edition.
- 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 |
46 | 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 |
312 | 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 |
60 | 0 | 0 | 0 | 0 | 0 | 14 | 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 2019.
Solver | Preliminary | Final | System description | Contact |
---|---|---|---|---|
version id | version id | for StarExec | ||
Asterix | 20618 | 20618 | Asterix | Juan Antonio Navarro PĂ©rez |
ComSPEN | 22337 | 22337 | ComSPEN | Chong Gao |
CVC4 | 20439 | 20439 | CVC4-SL | Andrew Reynolds |
Cyclist-SL | 1136 | 22685 | Cyclist-SL | Nikos Gorogiannis |
Harrsh | 22424 | 22687 | Harrsh | Jens Katelaan |
S2S | 22394 | 22440 | S2S | Le Quang Loc |
Sleek | 20564 | 20564 | Sleek | Benedict Lee |
Slide | 20623 | 20623 | Slide | Adam Rogalewicz |
SLSAT | 1137 | 22694 | SLSAT | Nikos Gorogiannis |
Songbird | 20617 | 20617 | Songbird | Ta Quang Trung |
SPEN | 20561 | 22729 | SPEN | Mihaela Sighireanu |
These are the benchmark divisions in which each solver is competing:
Division | #prob | Asterix | ComSPEN | CVC4 | Cyclist | Harrsh | S2S | Sleek | Slide | SLSAT | Songbird | SPEN |
---|---|---|---|---|---|---|---|---|---|---|---|---|
qf_bsl_sat |
46 | X | ||||||||||
qf_bsllia_sat |
24 | X | ||||||||||
qf_shid_entl |
312 | X | X | X | X | X | X | |||||
qf_shid_sat |
99 | X | X | X | X | X | ||||||
qf_shidlia_entl |
61 | X | X | X | X | |||||||
qf_shidlia_sat |
33 | X | X | X | X | |||||||
qf_shlid_entl |
60 | X | X | X | X | X | X | X | X | |||
qf_shls_entl |
296 | X | X | X | X | X | X | X | X | X | ||
qf_shls_sat |
110 | X | X | X | X | X | X | X | X | |||
shid_entl |
73 | X | X | X | X | X | ||||||
shidlia_entl |
181 | X | X | X |
Results
- Two runs took place between March 8th and April 3rd, 2019.
- The final results will be announced at TOOLympics during TACAS 2019.
- The results are provided below using the following glossary.
Committee
This edition is run by Mihaela Sighireanu.
The competition committee includes 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.