# 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 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

A set of new problems proposed for division `qf_{shid}_{entl}` 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.