Verification Witnesses from Verification Tools (SV-COMP 2023)

<strong>SV-COMP 2023</strong> <strong>Verification Witnesses</strong> This file describes the contents of an archive of the 12th Competition on Software Verification (SV-COMP 2023). https://sv-comp.sosy-lab.org/2023/ The competition was organized by Dirk Beyer, LMU Munich, Germany. More information is available in the following article: Dirk Beyer. <em>Competition on Software Verification and Witness Validation: SV-COMP 2023.</em> In Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023, Munich, April 22 - 27), 2023. Springer. Copyright (C) Dirk Beyer https://www.sosy-lab.org/people/beyer/ SPDX-License-Identifier: CC-BY-4.0 https://spdx.org/licenses/CC-BY-4.0.html <strong>Contents</strong> <code>LICENSE.txt</code>: specifies the license <code>README.txt</code>: this file <code>witnessFileByHash/</code>: This directory contains verification witnesses. Each verification witness in this directory is stored in a file whose name is the SHA2 256-bit hash of its contents followed by the filename extension .graphml. The format of each verification witness is described on the format web page: https://github.com/sosy-lab/sv-witnesses/ A verification witness contains also metadata in order to relate it to the verification task for which it was produced. <code>witnessInfoByHash/</code>: This directory contains for each verification witness in directory witnessFileByHash/ a record in JSON format (also using the SHA2 256-bit hash of the witness as filename, with .json as filename extension) that contains the meta data. <code>witnessListByProgramHashJSON/</code>: For convenient access to all verification witnesses for a certain program, this directory represents a function that maps each program (via its SHA2256-bit hash) to a set of verification witnesses (JSON records for verification witnesses as described above) that the verification tools have produced for that program. For each program for which verification witnesses exist, the directory contains a JSON file (using the SHA2 256-bit hash of the program as filename, with .json as filename extension) that contains all JSON records for verification witnesses for that program. The data structure is described in the following article: Dirk Beyer. <em>A Data Set of Program Invariants and Error Paths.</em> In Proceedings of the 2019 IEEE/ACM 16th International Conference on Mining Software Repositories (MSR 2019, Montreal, Canada, May 26-27), pages 111-115, 2019. IEEE. https://doi.org/10.1109/MSR.2019.00026 <strong>Other Archives</strong> Overview over archives from SV-COMP 2023 that are available at Zenodo: https://doi.org/10.5281/zenodo.7627791 Verification Witnesses from SV-COMP 2023 Verification Tools. Witness store (containing the generated verification witnesses) https://doi.org/10.5281/zenodo.7627829 Tool Archives from SV-COMP 2023. Executable tools that were evaluated in the competition https://doi.org/10.5281/zenodo.7627787 Results of the 12th Intl. Competition on Software Verification (SV-COMP 2023). Results (XML result files, log files, file mappings, HTML tables) https://doi.org/10.5281/zenodo.7627783 SV-Benchmarks: Benchmark Set of SV-COMP 2023 and Test-Comp 2023. Verification tasks, version svcomp23 https://doi.org/10.5281/zenodo.7612021 BenchExec, version 3.16. Benchmarking framework All benchmarks were executed for SV-COMP 2023 https://sv-comp.sosy-lab.org/2023/ by Dirk Beyer, LMU Munich, based on the following components: https://gitlab.com/sosy-lab/sv-comp/archives-2023 svcomp23 ca51c0c69ed4d4f6fd867c10abbc9b000d8ffb03 https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks svcomp23 f87854c275a177e8dc3673fe6959cd89038652af https://gitlab.com/sosy-lab/sv-comp/bench-defs svcomp23 d34d04f1332a49c219293798b90eee6b3760946d https://gitlab.com/sosy-lab/software/benchexec 3.16 b43e7384112770a41b571399135065daa7f387ab https://gitlab.com/sosy-lab/benchmarking/competition-scripts svcomp23 e6f84b5a79626b4295108a0f96ea370edde1f023 https://github.com/sosy-lab/sv-witnesses svcomp23 e16b1fdddfa7770918c2d06bdcd0103e88e32691 https://gitlab.com/sosy-lab/software/coveriteam svcomp23 76a8e4dba327af4606e2a30544656b7882f75848 <strong>Contact</strong> Feel free to contact me in case of questions: https://www.sosy-lab.org/people/beyer/<strong>SV-COMP 2023 验证见证集</strong> 本文档用于说明第十二届软件验证竞赛（SV-COMP 2023）归档包的内容。相关官网地址：https://sv-comp.sosy-lab.org/2023/ 本次竞赛由德国慕尼黑路德维希-马克西米利安大学的Dirk Beyer组织。更多详细信息可参阅以下论文：Dirk Beyer. *软件验证与见证验证竞赛：SV-COMP 2023*。发表于第29届软件构建与分析系统国际工具与算法大会（TACAS 2023，德国慕尼黑，4月22日-27日），2023年，Springer出版社。 版权所有 © Dirk Beyer，详见：https://www.sosy-lab.org/people/beyer/。本作品采用知识共享署名4.0国际许可协议（CC-BY-4.0）进行许可，许可详情可访问：https://spdx.org/licenses/CC-BY-4.0.html <strong>内容说明</strong> <code>LICENSE.txt</code>：说明本归档的许可协议 <code>README.txt</code>：本文档 <code>witnessFileByHash/</code>：该目录存储验证见证文件。目录内的每个验证见证均以其内容的SHA2 256位哈希值作为文件名，后缀为.graphml。验证见证的格式说明可参阅格式文档页面：https://github.com/sosy-lab/sv-witnesses/。每个验证见证均包含元数据，用于关联其对应的待验证任务。 <code>witnessInfoByHash/</code>：该目录为<code>witnessFileByHash/</code>目录下的每个验证见证提供一条JSON格式的元数据记录，文件名同样采用验证见证的SHA2 256位哈希值，后缀为.json。 <code>witnessListByProgramHashJSON/</code>：为便于检索特定程序对应的所有验证见证，该目录提供了一个映射关系：以程序的SHA2 256位哈希值为键，映射至验证工具为该程序生成的所有验证见证集合（即前文所述的JSON格式验证见证记录）。对于存在验证见证的程序，该目录下会包含一个以程序的SHA2 256位哈希值作为文件名、后缀为.json的JSON文件，其中存储了该程序对应的所有验证见证的JSON记录。该数据结构的详细说明可参阅以下论文：Dirk Beyer. *程序不变量与错误路径数据集*。发表于2019年IEEE/ACM第16届软件仓库挖掘国际会议（MSR 2019，加拿大蒙特利尔，5月26日-27日），第111-115页，2019年，IEEE出版社。DOI：https://doi.org/10.1109/MSR.2019.00026 <strong>其他归档包</strong> Zenodo平台上可获取的SV-COMP 2023系列归档包概览：https://doi.org/10.5281/zenodo.7627791 - SV-COMP 2023验证工具验证见证集：存储竞赛中生成的验证见证文件，DOI：https://doi.org/10.5281/zenodo.7627829 - SV-COMP 2023工具归档包：竞赛中使用的参评可执行工具集，DOI：https://doi.org/10.5281/zenodo.7627787 - 第十二届国际软件验证竞赛（SV-COMP 2023）结果集：包含XML结果文件、日志文件、文件映射表及HTML表格等竞赛结果，DOI：https://doi.org/10.5281/zenodo.7627783 - SV-Benchmarks：SV-COMP 2023与Test-Comp 2023的基准测试集，包含验证任务，版本为svcomp23，DOI：https://doi.org/10.5281/zenodo.7612021 BenchExec 3.16版：基准测试框架。本数据集所有基准测试均由德国慕尼黑路德维希-马克西米利安大学的Dirk Beyer基于以下组件为SV-COMP 2023执行完成： https://gitlab.com/sosy-lab/sv-comp/archives-2023 svcomp23 ca51c0c69ed4d4f6fd867c10abbc9b000d8ffb03 https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks svcomp23 f87854c275a177e8dc3673fe6959cd89038652af https://gitlab.com/sosy-lab/sv-comp/bench-defs svcomp23 d34d04f1332a49c219293798b90eee6b3760946d https://gitlab.com/sosy-lab/software/benchexec 3.16 b43e7384112770a41b571399135065daa7f387ab https://gitlab.com/sosy-lab/benchmarking/competition-scripts svcomp23 e6f84b5a79626b4295108a0f96ea370edde1f023 https://github.com/sosy-lab/sv-witnesses svcomp23 e16b1fdddfa7770918c2d06bdcd0103e88e32691 https://gitlab.com/sosy-lab/software/coveriteam svcomp23 76a8e4dba327af4606e2a30544656b7882f75848 <strong>联系方式</strong> 如有任何疑问，欢迎联系：https://www.sosy-lab.org/people/beyer/