SL-COMP 2018

Table of Contents

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

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 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:
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 75 0 22 0 0 0 0 0 0 53 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 75   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_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: 75 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

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.

Previous SL-COMPs

Author: Mihaela Sighireanu

Created: 2018-07-15 Sun 08:03

Validate