SL-COMP: Competition of Solvers for Separation Logic

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; Tomas Vojnar; Constantin Enea; Ondrej Lengal; Chong  Gao; Zhilin Wu

doi:10.1007/978-3-030-17502-3_8

SL-COMP: Competition of Solvers for Separation Logic

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, Tomas VojnarConstantin Enea, Ondrej Lengal, Chong Gao, Zhilin Wu

Research output: Chapter in Book/Report/Conference proceeding › Chapter (peer-reviewed) › peer-review

144 Downloads (Pure)

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.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of {TACAS:} TOOLympics, Held as Part of {ETAPS} 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part {III}
Subtitle of host publication	TOOLympics, Held as Part of ETAPS 2019, Proceedings
Editors	Fabrice Kordon, Marieke Huisman, Bernhard Steffen, Dirk Beyer
Publisher	Springer
Pages	116
Number of pages	16
Volume	11429
ISBN (Electronic)	978-3-030-17501-6
ISBN (Print)	978-3-030-17501-6
DOIs	https://doi.org/10.1007/978-3-030-17502-3_8
Publication status	E-pub ahead of print - 4 Apr 2019

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	11429 LNCS

Access to Document

10.1007/978-3-030-17502-3_8

SL-COMP Competition of Solvers for Separation LogicFinal published version, 350 KBLicence: CC BY

Cite this

Sighireanu, M., Pérez, J. A. N., Rybalchenko, A., Gorogiannis, N., Iosif, R., Reynolds, A., Serban, C., Katelaan, J., Matheja, C., Noll, T., Zuleger, F., Chin, W.-N., Le, Q. L., Ta, Q.-T., Le, T. C., Nguyen, T.-T., Khoo, S.-C., Cyprian, M., Rogalewicz, A., ... Wu, Z. (2019). SL-COMP: Competition of Solvers for Separation Logic. In F. Kordon, M. Huisman, B. Steffen, & D. Beyer (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of {TACAS:} TOOLympics, Held as Part of {ETAPS} 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part {III}: TOOLympics, Held as Part of ETAPS 2019, Proceedings (Vol. 11429, pp. 116). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11429 LNCS). Springer. Advance online publication. https://doi.org/10.1007/978-3-030-17502-3_8

Sighireanu, Mihaela ; Pérez, Juan A. Navarro ; Rybalchenko, Andrey et al. / SL-COMP: Competition of Solvers for Separation Logic. Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of {TACAS:} TOOLympics, Held as Part of {ETAPS} 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part {III}: TOOLympics, Held as Part of ETAPS 2019, Proceedings. editor / Fabrice Kordon ; Marieke Huisman ; Bernhard Steffen ; Dirk Beyer. Vol. 11429 Springer, 2019. pp. 116 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inbook{1217b45a3dcd4bdaac1f75f73cef3a05,

title = "SL-COMP: Competition of Solvers for Separation Logic",

abstract = "SL-COMP aims at bringing together researchers interestedon improving the state of the art of the automated deduction methodsfor Separation Logic (SL). The event took place twice until now and collectedmore than 1K problems for different fragments of SL. The inputformat of problems is based on the SMT-LIB format and therefore fullytyped; only one new command is added to SMT-LIB{\textquoteright}s list, the commandfor the declaration of the heap{\textquoteright}s type. The SMT-LIB theory ofSL comes with ten logics, some of them being combinations of SL withlinear arithmetics. The competition{\textquoteright}s divisions are defined by the logicfragment, the kind of decision problem (satisfiability or entailment) andthe presence of quantifiers. Until now, SL-COMP has been run on theStarExec platform, where the benchmark set and the binaries of participantsolvers are freely available. The benchmark set is also available withthe competition{\textquoteright}s documentation on a public repository in GitHub.",

author = "Mihaela Sighireanu and P{\'e}rez, {Juan A. Navarro} 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 Le, {Quang Loc} and Quang-Trung Ta and Le, {Ton Chanh} and Thanh-Toan Nguyen and Siau-Cheng Khoo and Michal Cyprian and Adam Rogalewicz and Tomas Vojnar and Constantin Enea and Ondrej Lengal and Chong Gao and Zhilin Wu",

year = "2019",

month = apr,

day = "4",

doi = "10.1007/978-3-030-17502-3_8",

language = "English",

isbn = "978-3-030-17501-6",

volume = "11429",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "116",

editor = "Fabrice Kordon and Marieke Huisman and Bernhard Steffen and Dirk Beyer",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of {TACAS:} TOOLympics, Held as Part of {ETAPS} 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part {III}",

}

Sighireanu, M, Pérez, JAN, Rybalchenko, A, Gorogiannis, N, Iosif, R, Reynolds, A, Serban, C, Katelaan, J, Matheja, C, Noll, T, Zuleger, F, Chin, W-N, Le, QL, Ta, Q-T, Le, TC, Nguyen, T-T, Khoo, S-C, Cyprian, M, Rogalewicz, A, Vojnar, T, Enea, C, Lengal, O, Gao, C & Wu, Z 2019, SL-COMP: Competition of Solvers for Separation Logic. in F Kordon, M Huisman, B Steffen & D Beyer (eds), Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of {TACAS:} TOOLympics, Held as Part of {ETAPS} 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part {III}: TOOLympics, Held as Part of ETAPS 2019, Proceedings. vol. 11429, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11429 LNCS, Springer, pp. 116. https://doi.org/10.1007/978-3-030-17502-3_8

SL-COMP: Competition of Solvers for Separation Logic. / Sighireanu, Mihaela ; Pérez, Juan A. Navarro; Rybalchenko, Andrey et al.
Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of {TACAS:} TOOLympics, Held as Part of {ETAPS} 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part {III}: TOOLympics, Held as Part of ETAPS 2019, Proceedings. ed. / Fabrice Kordon; Marieke Huisman; Bernhard Steffen; Dirk Beyer. Vol. 11429 Springer, 2019. p. 116 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11429 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Chapter (peer-reviewed) › peer-review

TY - CHAP

T1 - SL-COMP: Competition of Solvers for Separation Logic

AU - Sighireanu, Mihaela

AU - Pérez, Juan A. Navarro

AU - Rybalchenko, Andrey

AU - Gorogiannis, Nikos

AU - Iosif, Radu

AU - Reynolds, Andrew

AU - Serban, Cristina

AU - Katelaan, Jens

AU - Matheja, Christoph

AU - Noll, Thomas

AU - Zuleger, Florian

AU - Chin, Wei-Ngan

AU - Le, Quang Loc

AU - Ta, Quang-Trung

AU - Le, Ton Chanh

AU - Nguyen, Thanh-Toan

AU - Khoo, Siau-Cheng

AU - Cyprian, Michal

AU - Rogalewicz, Adam

AU - Vojnar, Tomas

AU - Enea, Constantin

AU - Lengal, Ondrej

AU - Gao, Chong

AU - Wu, Zhilin

PY - 2019/4/4

Y1 - 2019/4/4

N2 - SL-COMP aims at bringing together researchers interestedon improving the state of the art of the automated deduction methodsfor Separation Logic (SL). The event took place twice until now and collectedmore than 1K problems for different fragments of SL. The inputformat of problems is based on the SMT-LIB format and therefore fullytyped; only one new command is added to SMT-LIB’s list, the commandfor the declaration of the heap’s type. The SMT-LIB theory ofSL comes with ten logics, some of them being combinations of SL withlinear arithmetics. The competition’s divisions are defined by the logicfragment, the kind of decision problem (satisfiability or entailment) andthe presence of quantifiers. Until now, SL-COMP has been run on theStarExec platform, where the benchmark set and the binaries of participantsolvers are freely available. The benchmark set is also available withthe competition’s documentation on a public repository in GitHub.

AB - SL-COMP aims at bringing together researchers interestedon improving the state of the art of the automated deduction methodsfor Separation Logic (SL). The event took place twice until now and collectedmore than 1K problems for different fragments of SL. The inputformat of problems is based on the SMT-LIB format and therefore fullytyped; only one new command is added to SMT-LIB’s list, the commandfor the declaration of the heap’s type. The SMT-LIB theory ofSL comes with ten logics, some of them being combinations of SL withlinear arithmetics. The competition’s divisions are defined by the logicfragment, the kind of decision problem (satisfiability or entailment) andthe presence of quantifiers. Until now, SL-COMP has been run on theStarExec platform, where the benchmark set and the binaries of participantsolvers are freely available. The benchmark set is also available withthe competition’s documentation on a public repository in GitHub.

UR - http://www.scopus.com/inward/record.url?scp=85064929092&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-17502-3_8

DO - 10.1007/978-3-030-17502-3_8

M3 - Chapter (peer-reviewed)

SN - 978-3-030-17501-6

VL - 11429

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 116

BT - Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of {TACAS:} TOOLympics, Held as Part of {ETAPS} 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part {III}

A2 - Kordon, Fabrice

A2 - Huisman, Marieke

A2 - Steffen, Bernhard

A2 - Beyer, Dirk

PB - Springer

ER -

Sighireanu M, Pérez JAN, Rybalchenko A, Gorogiannis N, Iosif R, Reynolds A et al. SL-COMP: Competition of Solvers for Separation Logic. In Kordon F, Huisman M, Steffen B, Beyer D, editors, Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of {TACAS:} TOOLympics, Held as Part of {ETAPS} 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part {III}: TOOLympics, Held as Part of ETAPS 2019, Proceedings. Vol. 11429. Springer. 2019. p. 116. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Epub 2019 Apr 4. doi: 10.1007/978-3-030-17502-3_8

SL-COMP: Competition of Solvers for Separation Logic

Abstract

Publication series

Access to Document

Other files and links

Fingerprint

Cite this