Competition of Solvers for Separation Logic

This page describes the solvers that have participated to at least one edition of SL-COMP.


The solver deals with the satisfiability and entailment checking in the QF_SHLS fragment. For this, it implements a model-based approach. The procedure relies on SMT solving technology (Z3 solver is used) to untangle potential aliasing between program variables. It has at its core a matching function that checks whether a concrete valuation is a model of the input formula and, if so, generalizes it to a larger class of models where the formula is also valid.


ComSPEN (for Compositional SPEN) is a solver for the symbolic heap fragment of SL with compositional ID. It also supports linear integer arithmetics.


Cyclist-SL deals with the entailment checking for the QF_SLID fragment. It is an instantiation of the theorem prover Cyclist for the case of Separation Logic with inductive definitions. The solver builds derivation trees and uses induction to cut infinite paths in these trees that satisfy some soundness condition. For the Separation Logic, Cyclist-SL replaces the rule of weakening used in first-order theorem provers with the frame rule of SL.


CVC4-SL includes a procedure for the boolean combination of SL atoms without inductive definitions.


HARRSH is a prover for symbolic heap separation logic with user defined predicates. It can prove satisfiability as well as various reachability based properties of symbolic heaps, including garbage freedom and acyclicity. HARRSH is based on Heap Automata, as introduced in our ESOP 2017 paper below.


S2S is a Solver for Second-order Separation logic. It supports constraints in separation logic combining with general inductive definitions, arithmetic and string. S2S includes a central component of a generic cyclic proof framework. Currently, three cyclic-proof instantiations have been implemented: two solvers of separation logic (one for satisfiability and one for entailment) and one satisfiability solver of string logic.


Sleek deals with the satisfiability and entailment checking for the qf_shid fragment. It is an (incomplete but) automatic prover, that builds a proof tree for the input problem by using the classical inference rules and the frame rule of SL. It also uses a database of lemmas for the inductive definitions in order to discharge the proof obligations on the spatial formulas. The proof obligations on pure formulas are discharged by external provers like CVC4, Mona, or Z3.


SLIDE is a tool for deciding entailments between two given predicates, from a larger system of inductively defined predicates, written in an existential fragment of Separation Logic. The proof method relies on converting both the left hand and right hand sides of the entailment into two tree automata AutLHS and AutRHS, respectively, and checking the tree language inclusion of the automaton AutLHS in the automaton AutRHS.


SLSAT deals with the satisfiability problem for the qf_slid fragment. The decision procedure is based on a fixed point computation of a constraint, called the base of an inductive predicate definition. This constraint is a conjunction of equalities and dis-equalities between a set of free variables built also by the fixed point computation from the set of inductive definitions.


Songbird targets shidlia fragment and its subfragments. It employs mathematical induction to prove entailments involving user-defined predicates. In addition, Songbird is also equipped with powerful proof techniques, which include a mutual induction proof system and a lemma synthesis framework.


SPEN is an open source solver for checking validity of entailments between formulas in a fragment of Separation Logic with inductive definitions and linear integer constraints. The internals are published in