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

  • June 24: deadline for solver registration
  • July 1: first round of the competition
  • July 8: 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 800 problems. This set includes the one in the 2014 edition and nerly 200 new problems. The current set of problems is split into the following divisions:
    • qf_shls_sat: sat problem for quantifier free formulas in the symbolic heaps fragment using only acyclic singly linked lists
    • qf_shls_entl: entailment problems for the above fragment
    • qf_shid_sat: sat problem for quantifier free formulas in the symbolic heaps fragment using general inductive definitions
    • qf_shid_entl: entailment problem for quantifier free formulas in the symbolic heaps fragment using general inductive definitions
    • qf_shlid_entl: entailment problem for quantifier free formulas in the symbolic heaps fragment using linear inductive definitions
    • shid_entl: entailment problem for formulas in the symbolic heaps fragment general inductive definitions
  • SL-COMP 2014 collected a set of 678 problems The problems collected have 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 symbolic heap fragment of Separation Logic with a unique inductive predicate specifying acyclic singly linked list.
      • sll0a_entl: entailment problems for the above fragment.
      • FDB_entl: entailment problems for the symbolic heap fragment of Separation Logic with linear inductive definitions specifying various kinds of lists in a restricted way.
      • UDB_sat: satisfiability problems for the symbolic heap fragment of Separation Logic with general, user defined inductive definitions specifying lists, trees, etc.

Participants

The final list of participants will be announces June 25th, 2018. Some participants already confimed their presence to SL-COMP'18:

  • Asterix: divisions qf_shls_sat and qf_shls_entl
  • COMP-SPEN: division qf_shlidlia_entl
  • Cyclist: all divisions
  • Harrsh: division qf_shls_sat
  • Inductor: divisions qf_shid_entl
  • Sleek: all divisions
  • SongBird: all divisions
  • SPEN: divisions qf_shls_sat, qf_shls_entl, qf_shlid_entl, and qf_shlidlia_entl

The list of participants at SL-COMP 2014 is provided here.

Results

The results will be announces July 13th, 2018, at the ADSL workshop.

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-06-18 Mon 11:09

Validate