SL-COMP: Competition of Solvers for Separation Logic
SL-COMP: Competition of Solvers for Separation Logic
复制标题
DOI：
10.1007/978-3-030-17502-3_8
复制
发表时间：
2019-04
期刊：
影响因子：
--
通讯作者：
M. Sighireanu;J. A. Pérez;A. Rybalchenko;Nikos Gorogiannis;Radu Iosif;Andrew Reynolds;Cristina Serban;Jens Katelaan;Christoph Matheja;T. Noll;Florian Zuleger;W. Chin;Quang Loc Le;Quang-Trung Ta;T. Le;Thanh-Toan Nguyen;Siau-Cheng Khoo;Michal Cyprian;Adam Rogalewicz;Tomáš Vojnar;C. Enea;Ondřej Lengál;Chong Gao;Zhilin Wu
中科院分区：
文献类型：
--
作者：
M. Sighireanu;J. A. Pérez;A. Rybalchenko;Nikos Gorogiannis;Radu Iosif;Andrew Reynolds;Cristina Serban;Jens Katelaan;Christoph Matheja;T. Noll;Florian Zuleger;W. Chin;Quang Loc Le;Quang-Trung Ta;T. Le;Thanh-Toan Nguyen;Siau-Cheng Khoo;Michal Cyprian;Adam Rogalewicz;Tomáš Vojnar;C. Enea;Ondřej Lengál;Chong Gao;Zhilin Wu
SL-COMP旨在将对改进分离逻辑(SL)的自动演绎方法的技术水平感兴趣的研究人员聚集在一起。到目前为止，该事件已经发生了两次，为SL的不同片段收集了超过1K个问题。问题的输入格式基于SMT-Lib格式，因此是完全类型化的；SMT-Lib的列表中只添加了一个新命令，即用于声明堆类型的命令。SL的SMT-LIB理论有十个逻辑，其中一些是SL与线性算术的组合。竞赛的划分由逻辑片段、决策问题的类型(可满足性或蕴涵)和量词的存在来定义。到目前为止，SL-COMP一直运行在StarExec平台上，在那里可以免费获得基准测试集和参与者求解器的二进制文件。GitHub的公共存储库中也提供了该基准测试集以及竞争对手的文档。
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.