Results of the 13th Intl. Competition on Software Verification (SV-COMP 2024)

SV-COMP 2024 Competition Results This file describes the contents of an archive of the 13th Competition on Software Verification (SV-COMP 2024). https://sv-comp.sosy-lab.org/2024/ The competition was organized by Dirk Beyer, LMU Munich, Germany. More information is available in the following article: Dirk Beyer. State of the Art in Software Verification and Witness Validation: SV-COMP 2024. In Proceedings of the 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2024, Luxembourg, April 6 - 11), 2024. 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 To browse the competition results with a web browser, there are two options: start a local web server using php -S localhost:8000 in order to view the data in this archive, or browse https://sv-comp.sosy-lab.org/2023/results/ in order to view the data on the SV-COMP web page. Contents index.html: directs to the overview web page of the verification track index-validation.html: directs to the overview web page of the validation track LICENSE-results.txt: specifies the license README-results.txt: this file results-validated/: results of validation runs results-verified/: results of verification runs The folder results-validated/ contains the results from validation runs: index.html: overview web page with rankings and score table design.css: HTML style definitions *.results.txt: TXT results from BenchExec *.xml.bz2: XML results from BenchExec *.fixed.xml.bz2: XML results from BenchExec, status adjusted according to the validation results *.logfiles.zip: output from tools *.json.gz: mapping from files names to SHA 256 hashes for the file content <validator>*.table.html: HTML views of the full benchmark set (all categories) for each validator <category>*.table.html: HTML views of the benchmark set for each category over all validators *.xml: XML table definitions for the above tables validators.*: Statistics of the validator runs (obsolete) .correctness.: Infix for validation of correctness witnesses .violation.: Infix for validation of violation witnesses quantilePlot-*: score-based quantile plots as visualization of the results quantilePlotShow.gp: example Gnuplot script to generate a plot score*: accumulated score results in various formats witness-database.csv: data base of all witnesses witness-classification.csv: data base of all witnesses with their classification into correct, wrong, unknown The folder results-verified/ contains the results from verification runs and aggregated results: index.html: overview web page with rankings and score table design.css: HTML style definitions *.results.txt: TXT results from BenchExec *.xml.bz2: XML results from BenchExec *.fixed.xml.bz2: XML results from BenchExec, status adjusted according to the validation results *.logfiles.zip: output from tools *.json.gz: mapping from files names to SHA 256 hashes for the file content *.xml.bz2.table.html: HTML views on the detailed results data as generated by BenchExec’s table generator <verifier>*.table.html: HTML views of the full benchmark set (all categories) for each verifier META_*.table.html: HTML views of the benchmark set for each meta category for each verifier, and over all verifiers <category>*.table.html: HTML views of the benchmark set for each category over all verifiers *.xml: XML table definitions for the above tables validatorStatistics.html: Statistics of the validator runs (obsolete) results-per-tool.php: List of results for each tool for review process in pre-run phase <verifier>.list.html: List of results for a tool in HTML format with links quantilePlot-*: score-based quantile plots as visualization of the results quantilePlotShow.gp: example Gnuplot script to generate a plot score*: accumulated score results in various formats The hashes of the file names (in the files *.json.gz) are useful for validating the exact contents of a file and accessing the files from the witness store. Other Archives Overview of archives from SV-COMP 2024 that are available at Zenodo: https://doi.org/10.5281/zenodo.10669737 Verification Witnesses from SV-COMP 2024 Verification Tools. Witness store (containing the generated verification witnesses) https://doi.org/10.5281/zenodo.10669735 Verifiers and Validators: FM-Tools Data Set for SV-COMP 2024. Metadata snapshot of the evaluated tools (DOIs, options, etc.) https://doi.org/10.5281/zenodo.10669731 Results of the 13th Intl. Competition on Software Verification (SV-COMP 2024). Results (XML result files, log files, file mappings, HTML tables) https://doi.org/10.5281/zenodo.10669723 SV-Benchmarks: Benchmark Set of SV-COMP 2024. Verification tasks, version svcomp24 https://doi.org/10.5281/zenodo.10671136 BenchExec, version 3.21. Benchmarking framework All benchmarks were executed for SV-COMP 2024 https://sv-comp.sosy-lab.org/2024/ by Dirk Beyer, LMU Munich, based on the following components: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks svcomp24 https://gitlab.com/sosy-lab/sv-comp/bench-defs svcomp24 https://github.com/sosy-lab/benchexec 3.21 https://gitlab.com/sosy-lab/benchmarking/fm-tools svcomp24 https://gitlab.com/sosy-lab/benchmarking/sv-witnesses svcomp24 https://gitlab.com/sosy-lab/software/coveriteam 1.1 https://gitlab.com/sosy-lab/benchmarking/competition-scripts svcomp24 Contact Feel free to contact me in case of questions: https://www.sosy-lab.org/people/beyer/SV-COMP 2024 竞赛结果 本文件描述第13届软件验证竞赛（SV-COMP 2024）归档包的内容，官方网址为 https://sv-comp.sosy-lab.org/2024/。 本次竞赛由德国慕尼黑大学LMU的Dirk Beyer组织。更多详细信息可参阅以下论文：Dirk Beyer. 软件验证与见证验证的最新进展：SV-COMP 2024. 发表于第30届国际工具与算法构造与分析大会（TACAS 2024，卢森堡，4月6日-11日），2024年，Springer出版社。 版权所有 © Dirk Beyer https://www.sosy-lab.org/people/beyer/ SPDX许可标识符：知识共享署名4.0国际许可协议（CC-BY-4.0），详情见 https://spdx.org/licenses/CC-BY-4.0.html 若需通过网页浏览器浏览竞赛结果，可选择以下两种方式： 1. 在本地启动Web服务器：在命令行执行`php -S localhost:8000`以查看本归档包内的数据； 2. 直接访问SV-COMP官方网页的结果页面：https://sv-comp.sosy-lab.org/2023/results/ ## 归档内容 - `index.html`：指向软件验证赛道的概览网页 - `index-validation.html`：指向见证验证赛道的概览网页 - `LICENSE-results.txt`：说明本归档的许可协议 - `README-results.txt`：本说明文件 - `results-validated/`：见证验证运行的结果 - `results-verified/`：软件验证运行与聚合结果 ### `results-validated/` 文件夹：包含见证验证运行的结果 - `index.html`：包含排名与评分表的概览网页 - `design.css`：HTML样式定义文件 - `*.results.txt`：BenchExec生成的TXT格式结果文件 - `*.xml.bz2`：BenchExec生成的XML格式结果文件 - `*.fixed.xml.bz2`：经验证结果调整后状态的BenchExec XML格式结果文件 - `*.logfiles.zip`：参赛工具的输出日志压缩包 - `*.json.gz`：文件名与文件内容SHA-256哈希值的映射文件 - `<validator>*.table.html`：各验证器的全基准集（含所有类别）HTML视图 - `<category>*.table.html`：所有验证器针对单个类别的基准集HTML视图 - `*.xml`：上述HTML表格对应的XML表格定义文件 - `validators.*`：验证器运行统计数据（已废弃） - `.correctness.`：正确性见证验证的中缀标识 - `.violation.`：违规见证验证的中缀标识 - `quantilePlot-*`：基于评分的分位数图，用于结果可视化 - `quantilePlotShow.gp`：用于生成分位数图的Gnuplot示例脚本 - `score*`：多种格式的累计评分结果文件 - `witness-database.csv`：所有见证的数据库文件 - `witness-classification.csv`：所有见证的分类数据库，包含正确、错误、未知三类标注 ### `results-verified/` 文件夹：包含软件验证运行结果与聚合结果 - `index.html`：包含排名与评分表的概览网页 - `design.css`：HTML样式定义文件 - `*.results.txt`：BenchExec生成的TXT格式结果文件 - `*.xml.bz2`：BenchExec生成的XML格式结果文件 - `*.fixed.xml.bz2`：经验证结果调整后状态的BenchExec XML格式结果文件 - `*.logfiles.zip`：参赛工具的输出日志压缩包 - `*.json.gz`：文件名与文件内容SHA-256哈希值的映射文件 - `*.xml.bz2.table.html`：BenchExec表格生成器生成的详细结果数据HTML视图 - `<verifier>*.table.html`：各验证器的全基准集（含所有类别）HTML视图 - `META_*.table.html`：各验证器针对单个元类别的基准集HTML视图，以及所有验证器的全局元类别视图 - `<category>*.table.html`：所有验证器针对单个类别的基准集HTML视图 - `*.xml`：上述HTML表格对应的XML表格定义文件 - `validatorStatistics.html`：验证器运行统计数据（已废弃） - `results-per-tool.php`：供预运行阶段评审流程使用的各工具结果列表页面 - `<verifier>.list.html`：单工具结果的HTML格式列表页面，包含相关链接 - `quantilePlot-*`：基于评分的分位数图，用于结果可视化 - `quantilePlotShow.gp`：用于生成分位数图的Gnuplot示例脚本 - `score*`：多种格式的累计评分结果文件 文件名的哈希值（存储于`*.json.gz`文件中）可用于以下场景： 1. 验证文件的精确内容完整性； 2. 从见证存储库中访问对应文件。 ## 其他归档 SV-COMP 2024的其他归档包可在Zenodo学术存档平台获取，详情如下： 1. https://doi.org/10.5281/zenodo.10669737：SV-COMP 2024验证工具生成的验证见证。包含生成的验证见证的见证存储库。 2. https://doi.org/10.5281/zenodo.10669735：验证器与验证工具：SV-COMP 2024的FM-Tools数据集。包含被评估工具的元数据快照（如DOI、运行参数等）。 3. https://doi.org/10.5281/zenodo.10669731：第13届国际软件验证竞赛（SV-COMP 2024）结果。包含结果文件（XML结果文件、日志文件、文件映射、HTML表格等）。 4. https://doi.org/10.5281/zenodo.10669723：SV-Benchmarks：SV-COMP 2024基准集。验证任务集，版本为svcomp24。 5. https://doi.org/10.5281/zenodo.10671136：BenchExec 3.21版本。基准测试框架。 所有基准测试均为SV-COMP 2024执行，官方网址为 https://sv-comp.sosy-lab.org/2024/，由德国慕尼黑大学LMU的Dirk Beyer主导执行，所用组件如下： - https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks svcomp24 - https://gitlab.com/sosy-lab/sv-comp/bench-defs svcomp24 - https://github.com/sosy-lab/benchexec 3.21 - https://gitlab.com/sosy-lab/benchmarking/fm-tools svcomp24 - https://gitlab.com/sosy-lab/benchmarking/sv-witnesses svcomp24 - https://gitlab.com/sosy-lab/software/coveriteam 1.1 - https://gitlab.com/sosy-lab/benchmarking/competition-scripts svcomp24 ## 联系方式 如有任何疑问，可通过以下链接联系作者：https://www.sosy-lab.org/people/beyer/