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 proceedingChapter (peer-reviewed)

    109 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 languageEnglish
    Title of host publicationTools 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 publicationTOOLympics, Held as Part of ETAPS 2019, Proceedings
    EditorsFabrice Kordon, Marieke Huisman, Bernhard Steffen, Dirk Beyer
    PublisherSpringer
    Pages116
    Number of pages16
    Volume11429
    ISBN (Electronic)978-3-030-17501-6
    ISBN (Print)978-3-030-17501-6
    DOIs
    Publication statusE-pub ahead of print - 4 Apr 2019

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume11429 LNCS

    Fingerprint Dive into the research topics of 'SL-COMP: Competition of Solvers for Separation Logic'. Together they form a unique fingerprint.

  • 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. https://doi.org/10.1007/978-3-030-17502-3_8