Skip to content
Competition of Solvers for Separation Logic
CSS
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
assets/css
docs
README.md
_config.yml
sl-comp-wand.pdf
sl-comp-wand.svg
sl-comp.png

README.md

The Separation Logic Competition (SL-COMP) is an initiative to bring together researchers and practitioners interested on improving the state of the art of automated deduction methods for Separation Logic. The competition is run on more than 1K decision problems for different theories of Separation Logic. The solvers are compared on each theory on the number of problems solved and the running time. This initiative started at FLOC 2014 and it has been afiliated with different events: SMT-COMP 2014, FLOC 2018 workshop ADSL 2018 and TOOLympics 2019.

NEWS

Specification and rules

The competition compares solvers for decision problems in Separation Logic with respect to effectiveness and running time. The competition consists of two phases: a training phase, in which solver developers try their tool on the competition benchmark and may provide feedback to organizers, and an evaluation phase, in which all participating solvers are executed on benchmark problems, and the number of correctly solved instances as well as the runtime is measured.

A decision problem is either a satisfiability or an entailment problem in a fixed fragment of Separation Logic. The possible answers of a solver are: sat, unsat and unknown. The answer is compared with the known status of the problem specified in the problem's file. The result of the comparison determines the evaluation of the solver on this problem, which is correct, incorrect or unsolved.

The problems are specified using the format described here and commented in this post. The input format of problems extends the format SMT-LIB with SL constructs, and exploit the new features of SMT-LIB like datatypes definition and mutually recursive functions.

Teams may contribute with problems in the input format above. The number of problems submitted by a team in some division is limited. The problems submitted are revised by the organizing committee which may or may not accept it. An accepted problem may be changed when this improves the overall quality of the final set of problems.

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 time spent on this pre-processor is not included in the evaluation time. The input problems are not scrambled before their submission to he solver.

Benchmark and divisions

The set of decision problems collected until now are available for browsing and download on the following GIT repository.

Each problem is contributed by a team, as specified in the file header. Thanks to all participants that contributed programs, sent patches, and commented on the sets.

The file header also specifies the status of the problems (sat, unsat) and, most importantly, the logic fragment used in this problem. A division is defined by its logic fragment. The following division are now present:

  • 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 enter in the competition
    • 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

Tools

The GIT repository provides tools for parsing the input format (in C, C++ and Ocaml). Based on these tools, the organizing committee provides pre-processors of this input to solvers' input format.

The same repository includes a translator of the input format used for SL-COMP 2014 to the new input format.

Participants

The following solvers have participated to at least one edition of SL-COMP:

Editions

Papers

  • M. Sighireanu et al. SL-COMP: Competition of Solvers for Separation Logic. TOOLympics'19. PDF
  • R. Iosif, C. Serban, A. Reynolds, and M. Sighireanu. Encoding Separation Logic in SMT-LIB v2.5. PDF
  • M. Sighireanu and D. R. Cok. Report on SLCOMP 2014. JSAT 2014, PDF

Mailing list

Any question related to this competition shall be sent to the organisation committee and to the mailing list.

You can’t perform that action at this time.