SL-COMP: Competition of Solvers for Separation Logic
The work
| Authors | Mihaela Sighireanu; Juan A. Navarro Pérez; Andrey Rybalchenko; Nikos Gorogiannis; Radu Iosif; Andrew Reynolds; Cristina Serban; Jens Katelaan; Christoph Matheja; Thomas Noll; Florian Zuleger; Wei-Ngan Chin; Quang Loc Le; Quang-Trung Ta; Ton-Chanh Le; Thanh-Toan Nguyen; Siau-Cheng Khoo; Michal Cyprian; Adam Rogalewicz; Tomáš Vojnar; Constantin Enea; Ondřej Lengál; Chong Gao; Zhilin Wu |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2019 |
| Citekey | sighireanu2019sl |
Where it appeared
| Published in | International Conference on Tools and Algorithms for the Construction and Analysis of Systems |
|---|---|
| Publisher | Springer |
| Series | Lecture Notes in Computer Science |
| Pages | 116--132 |
Identifiers
| DOI | 10.1007/978-3-030-17502-3_8 |
|---|---|
| OpenAlex | W2929347481 |
| ISBN | 978-3-030-17501-6 |
Access
| Landing page | https://doi.org/10.1007/978-3-030-17502-3_8 |
|---|---|
| Free full text | https://link.springer.com/content/pdf/10.1007%2F978-3-030-17502-3_8.pdf |
Abstract
SL-COMP aims at bringing together researchers interested on improving the state of the art of the automated deduction methods for Separation Logic (SL). The event took place twice until now and collected more than 1K problems for different fragments of SL. The input format of problems is based on the SMT-LIB format and therefore fully typed; only one new command is added to SMT-LIB's list, the command for the declaration of the heap's type. The SMT-LIB theory of SL comes with ten logics, some of them being combinations of SL with linear arithmetics. The competition's divisions are defined by the logic fragment, the kind of decision problem (satisfiability or entailment) and the presence of quantifiers. Until now, SL-COMP has been run on the StarExec platform, where the benchmark set and the binaries of participant solvers are freely available. The benchmark set is also available with the competition's documentation on a public repository in GitHub.
A copy is held
pdf, 320.3 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-26 14:31 UTC |
Filed under
andrewreynolds chin gorogiannis iosif lncs quangloc separation-logic serban
Cite it as
@inproceedings{sighireanu2019sl,
title = {SL-COMP: Competition of Solvers for Separation Logic},
author = {Mihaela Sighireanu and Juan A. Navarro Pérez and Andrey Rybalchenko and Nikos Gorogiannis and Radu Iosif and Andrew Reynolds and Cristina Serban and Jens Katelaan and Christoph Matheja and Thomas Noll and Florian Zuleger and Wei-Ngan Chin and Quang Loc Le and Quang-Trung Ta and Ton-Chanh Le and Thanh-Toan Nguyen and Siau-Cheng Khoo and Michal Cyprian and Adam Rogalewicz and Tomáš Vojnar and Constantin Enea and Ondřej Lengál and Chong Gao and Zhilin Wu},
year = {2019},
booktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
pages = {116--132},
isbn = {978-3-030-17501-6},
doi = {10.1007/978-3-030-17502-3_8},
}
This record lives at https://refs.drheap.org/sighireanu2019sl/ and will keep doing so.