SL-COMP 2019

Table of Contents

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

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 `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.

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

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.

Author: Mihaela Sighireanu

Created: 2019-04-07 Sun 16:36

Validate