S2S: An Efficient Solver for Separation Logic

About S2S

S2S is an efficient and automatic decision procedure for problems in separation logic extended with string constraints. It can be used to prove the validity of both entailment and satisfiability of separation/string logic formulas.

Features

entailment and satisfiability problems of separation logic with

  • inductive predicates
  • integer arithmetic
  • satisfiability problems of string logic with

  • concatenation
  • regular memberships
  • length constraints
  • Documentation

    Coming (hopefully) soon ...

    Download

    0.3.3 (March 2019 - tested on Ubuntu 14.04, Ubuntu 16.04 and Ubuntu 18.04).

    License: academic use only.

    Warranty information:

  • This version was dedicated to SL-COMP 2019. It is not an official release.
  • The tool may contain bugs; use it with your own risks: "saw it, send it, (and we will) sort it".
  • New features are actively developed and updated.
  • Developers

  • Quang Loc Le
  • Contact

    lequangloc@gmail.com for bug report and discussion.

    Acknowledgments

  • Mihaela Sighireanu, the Chair, and the contributors of SL-COMP. At the early stage of the development, S2S was tested mainly by the bechmarks of SL-COMP 2018.