Find research datasets worth reusing
Search datasets from major research repositories and use ShareScore to quickly assess how well each record supports discovery, access, and reuse.
14
datasets available to search
ShareScore release 0.9.0
Dataset results
14 results for “Software verification”
Dataset for : A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification
<p>We present a novel solution combining Large Language Model (LLM) capabilities with Formal Verification strategies to falsify and automatically repair software vulnerabilities. Initially, we employ Bounded Model Checking (BMC) to locate the software vulnerability and derive a counterexample. Relying on mathematical proofs, counterexamples provide evidence that the system behaves incorrectly or contains a vulnerability, thereby preventing the generation of false positive alerts. The counterexample that has been detected, along with the source code, are provided to the LLM engine. Our approach involves establishing a specialized prompt language for conducting code debugging and generation to understand the vulnerability's root cause and repair the code. Finally, we use BMC to verify the corrected version of the code generated by the LLM. As a proof of concept, we create \esbmcai based on the Efficient SMT-based Context-Bounded Model Checker (ESBMC) and a pre-trained Transformer model, specifically gpt-3.5-turbo, to detect and fix errors in C programs. We generated a dataset comprising $1{,}000$ C code samples, each consisting of $20$ to $50$ lines of C code. Experimental results show that our proposed method achieved an impressive success rate of up to $80$\% in repairing vulnerable code, encompassing buffer overflow, arithmetic overflow, and pointer dereference failures. To our knowledge, \esbmcai represents the first proposal for a pioneering initiative to integrate a Large Language Model (LLM) with software model checking. We advocate that this automated approach has the potential to incorporate into the software development lifecycle's continuous integration and deployment (CI/CD) process. </p> <p> </p> <p>The uploaded dataset contains 1000 codes, each comprising 20 to 50 lines of C code generated with gpt-3.5-turbo. The material also consists of a version of ESBMC statically compiled with all dependencies, a classifier script, and the output file.</p> <p> </p> <p> </p>
Results of the 10th Intl. Competition on Software Verification (SV-COMP 2021)
<p>Competition Results</p> <p>This file describes the contents of an archive of the 10th Competition on Software Verification (SV-COMP 2021).<br> <a href="https://sv-comp.sosy-lab.org/2021/">https://sv-comp.sosy-lab.org/2021/</a></p> <p>The competition was run by Dirk Beyer, LMU Munich, Germany.<br> More information is available in the following article:<br> Dirk Beyer. <em>Software Verification: 10th Comparative Evaluation (SV-COMP 2021).</em> In Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021, Luxembourg, March 27 - April 1), 2021. Springer.</p> <p>Copyright (C) Dirk Beyer<br> <a href="https://www.sosy-lab.org/people/beyer/">https://www.sosy-lab.org/people/beyer/</a></p> <p>SPDX-License-Identifier: CC-BY-4.0<br> <a href="https://spdx.org/licenses/CC-BY-4.0.html">https://spdx.org/licenses/CC-BY-4.0.html</a></p> <p>To browse the competition results with a web browser, there are two options:</p> <ul> <li>start a local web server using php -S localhost:8000 in order to view the data in this archive, or</li> <li>browse https://sv-comp.sosy-lab.org/2021/results/ in order to view the data on the SV-COMP web page.</li> </ul> <p>Contents</p> <ul> <li><code>index.html</code>: directs to the overview web page</li> <li><code>LICENSE.txt</code>: specifies the license</li> <li><code>README.txt</code>: this file</li> <li><code>results-validated/</code>: results of validation runs</li> <li><code>results-verified/</code>: results of verification runs and aggregated results</li> </ul> <p>The folder <code>results-validated/</code> contains the results from validation runs:</p> <ul> <li><code>*.xml.bz2</code>: XML results from BenchExec</li> <li><code>*.logfiles.zip</code>: output from tools</li> <li><code>*.json.gz</code>: mapping from files names to SHA 256 hashes for the file content</li> </ul> <p>The folder <code>results-verified/</code> contains the results from verification runs and aggregated results:</p> <ul> <li><code>index.html</code>: overview web page with rankings and score table</li> <li><code>*.xml.bz2</code>: XML results from BenchExec</li> <li><code>*.merged.xml.bz2</code>: XML results from BenchExec, status adjusted according to the validation results</li> <li><code>*.logfiles.zip</code>: output from tools</li> <li><code>*.json.gz</code>: mapping from files names to SHA 256 hashes for the file content</li> <li><code>*.xml.bz2.table.html</code>: HTML views on the detailed results data as generated by BenchExec’s table generator</li> <li><code>*.All.table.html</code>: HTML views of the full benchmark set (all categories) for each tool</li> <li><code>META_*.table.html</code>: HTML views of the benchmark set for each meta category for each tool, and over all tools</li> <li><code><category>*.table.html</code>: HTML views of the benchmark set for each category over all tools</li> <li><code>iZeCa0gaey.html</code>: HTML views per tool</li> <li> <p><code>validatorStatistics.html</code>: Statictics of the validator runs</p> </li> <li><code>quantilePlot-*</code>: score-based quantile plots as visualization of the results</li> <li><code>quantilePlotShow.gp</code>: example Gnuplot script to generate a plot</li> <li> <p><code>score*</code>: accumulated score results in various formats</p> </li> </ul> <p>The hashes of the file names (in the files *.json.gz) are useful for</p> <ul> <li>validating the exact contents of a file and</li> <li>accessing the files from the witness store.</li> </ul> <p>Other Archives</p> <p>Overview over archives from SV-COMP 2021 that are available at Zenodo:</p> <ul> <li><a href="https://doi.org/10.5281/zenodo.4459196">https://doi.org/10.5281/zenodo.4459196</a> Witness store (containing the generated verification witnesses)</li> <li><a href="https://doi.org/10.5281/zenodo.4458215">https://doi.org/10.5281/zenodo.4458215</a> Results (XML result files, log files, file mappings, HTML tables)</li> <li><a href="https://doi.org/10.5281/zenodo.4459126">https://doi.org/10.5281/zenodo.4459126</a> Verification tasks, version svcomp21</li> <li><a href="https://doi.org/10.5281/zenodo.4317433">https://doi.org/10.5281/zenodo.4317433</a> BenchExec, version 3.6</li> </ul> <p>All benchmarks were executed for SV-COMP 2021 <a href="https://sv-comp.sosy-lab.org/2021/">https://sv-comp.sosy-lab.org/2021/</a><br> by Dirk Beyer, LMU Munich, based on the following components:</p> <ul> <li><a href="https://gitlab.com/sosy-lab/sv-comp/archives-2021">https://gitlab.com/sosy-lab/sv-comp/archives-2021</a> svcomp21-0-g08c7a98</li> <li><a href="https://gitlab.com/sosy-lab/software/sv-benchmarks">https://gitlab.com/sosy-lab/software/sv-benchmarks</a> svcomp21-0-g4cc6b6d96a</li> <li><a href="https://gitlab.com/sosy-lab/software/benchexec">https://gitlab.com/sosy-lab/software/benchexec</a> 3.6-0-gb278ebbb</li> <li><a href="https://gitlab.com/sosy-lab/benchmarking/competition-scripts">https://gitlab.com/sosy-lab/benchmarking/competition-scripts</a> svcomp21-0-g8339740</li> <li><a href="https://gitlab.com/sosy-lab/sv-comp/bench-defs">https://gitlab.com/sosy-lab/sv-comp/bench-defs</a> svcomp21-0-ga57fe48</li> </ul> <p>Contact</p> <p>Feel free to contact me in case of questions: <a href="https://www.sosy-lab.org/people/beyer/">https://www.sosy-lab.org/people/beyer/</a></p>
Results of the 13th Intl. Competition on Software Verification (SV-COMP 2024)
<h1>SV-COMP 2024</h1> <h2>Competition Results</h2> <p>This file describes the contents of an archive of the 13th Competition on Software Verification (SV-COMP 2024). <a href="https://sv-comp.sosy-lab.org/2024/">https://sv-comp.sosy-lab.org/2024/</a></p> <p>The competition was organized by Dirk Beyer, LMU Munich, Germany. More information is available in the following article: Dirk Beyer. <em>State of the Art in Software Verification and Witness Validation: SV-COMP 2024.</em> 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.</p> <p>Copyright (C) Dirk Beyer <a href="https://www.sosy-lab.org/people/beyer/">https://www.sosy-lab.org/people/beyer/</a></p> <p>SPDX-License-Identifier: CC-BY-4.0 <a href="https://spdx.org/licenses/CC-BY-4.0.html">https://spdx.org/licenses/CC-BY-4.0.html</a></p> <p>To browse the competition results with a web browser, there are two options:</p> <ul> <li>start a local web server using php -S localhost:8000 in order to view the data in this archive, or</li> <li>browse <a href="https://sv-comp.sosy-lab.org/2023/results/">https://sv-comp.sosy-lab.org/2023/results/</a> in order to view the data on the SV-COMP web page.</li> </ul> <h2>Contents</h2> <ul> <li><code>index.html</code>: directs to the overview web page of the verification track</li> <li><code>index-validation.html</code>: directs to the overview web page of the validation track</li> <li><code>LICENSE-results.txt</code>: specifies the license</li> <li><code>README-results.txt</code>: this file</li> <li><code>results-validated/</code>: results of validation runs</li> <li><code>results-verified/</code>: results of verification runs</li> </ul> <p>The folder <code>results-validated/</code> contains the results from validation runs:</p> <ul> <li> <p><code>index.html</code>: overview web page with rankings and score table</p> </li> <li> <p><code>design.css</code>: HTML style definitions</p> </li> <li> <p><code>*.results.txt</code>: TXT results from BenchExec</p> </li> <li> <p><code>*.xml.bz2</code>: XML results from BenchExec</p> </li> <li> <p><code>*.fixed.xml.bz2</code>: XML results from BenchExec, status adjusted according to the validation results</p> </li> <li> <p><code>*.logfiles.zip</code>: output from tools</p> </li> <li> <p><code>*.json.gz</code>: mapping from files names to SHA 256 hashes for the file content</p> </li> <li> <p><code><validator>*.table.html</code>: HTML views of the full benchmark set (all categories) for each validator</p> </li> <li> <p><code><category>*.table.html</code>: HTML views of the benchmark set for each category over all validators</p> </li> <li> <p><code>*.xml</code>: XML table definitions for the above tables</p> </li> <li> <p><code>validators.*</code>: Statistics of the validator runs (obsolete)</p> </li> <li> <p><code>.correctness.</code>: Infix for validation of correctness witnesses</p> </li> <li> <p><code>.violation.</code>: Infix for validation of violation witnesses</p> </li> <li> <p><code>quantilePlot-*</code>: score-based quantile plots as visualization of the results</p> </li> <li> <p><code>quantilePlotShow.gp</code>: example Gnuplot script to generate a plot</p> </li> <li> <p><code>score*</code>: accumulated score results in various formats</p> </li> <li> <p><code>witness-database.csv</code>: data base of all witnesses</p> </li> <li> <p><code>witness-classification.csv</code>: data base of all witnesses with their classification into correct, wrong, unknown</p> </li> </ul> <p>The folder <code>results-verified/</code> contains the results from verification runs and aggregated results:</p> <ul> <li> <p><code>index.html</code>: overview web page with rankings and score table</p> </li> <li> <p><code>design.css</code>: HTML style definitions</p> </li> <li> <p><code>*.results.txt</code>: TXT results from BenchExec</p> </li> <li> <p><code>*.xml.bz2</code>: XML results from BenchExec</p> </li> <li> <p><code>*.fixed.xml.bz2</code>: XML results from BenchExec, status adjusted according to the validation results</p> </li> <li> <p><code>*.logfiles.zip</code>: output from tools</p> </li> <li> <p><code>*.json.gz</code>: mapping from files names to SHA 256 hashes for the file content</p> </li> <li> <p><code>*.xml.bz2.table.html</code>: HTML views on the detailed results data as generated by BenchExec’s table generator</p> </li> <li> <p><code><verifier>*.table.html</code>: HTML views of the full benchmark set (all categories) for each verifier</p> </li> <li> <p><code>META_*.table.html</code>: HTML views of the benchmark set for each meta category for each verifier, and over all verifiers</p> </li> <li> <p><code><category>*.table.html</code>: HTML views of the benchmark set for each category over all verifiers</p> </li> <li> <p><code>*.xml</code>: XML table definitions for the above tables</p> </li> <li> <p><code>validatorStatistics.html</code>: Statistics of the validator runs (obsolete)</p> </li> <li> <p><code>results-per-tool.php</code>: List of results for each tool for review process in pre-run phase</p> </li> <li> <p><code><verifier>.list.html</code>: List of results for a tool in HTML format with links</p> </li> <li> <p><code>quantilePlot-*</code>: score-based quantile plots as visualization of the results</p> </li> <li> <p><code>quantilePlotShow.gp</code>: example Gnuplot script to generate a plot</p> </li> <li> <p><code>score*</code>: accumulated score results in various formats</p> </li> </ul> <p>The hashes of the file names (in the files <code>*.json.gz</code>) are useful for</p> <ul> <li>validating the exact contents of a file and</li> <li>accessing the files from the witness store.</li> </ul> <h2>Other Archives</h2> <p>Overview of archives from SV-COMP 2024 that are available at Zenodo:</p> <ul> <li><a href="https://doi.org/10.5281/zenodo.10669737">https://doi.org/10.5281/zenodo.10669737</a> Verification Witnesses from SV-COMP 2024 Verification Tools. Witness store (containing the generated verification witnesses)</li> <li><a href="https://doi.org/10.5281/zenodo.10669735">https://doi.org/10.5281/zenodo.10669735</a> Verifiers and Validators: FM-Tools Data Set for SV-COMP 2024. Metadata snapshot of the evaluated tools (DOIs, options, etc.)</li> <li><a href="https://doi.org/10.5281/zenodo.10669731">https://doi.org/10.5281/zenodo.10669731</a> Results of the 13th Intl. Competition on Software Verification (SV-COMP 2024). Results (XML result files, log files, file mappings, HTML tables)</li> <li><a href="https://doi.org/10.5281/zenodo.10669723">https://doi.org/10.5281/zenodo.10669723</a> SV-Benchmarks: Benchmark Set of SV-COMP 2024. Verification tasks, version svcomp24</li> <li><a href="https://doi.org/10.5281/zenodo.10671136">https://doi.org/10.5281/zenodo.10671136</a> BenchExec, version 3.21. Benchmarking framework</li> </ul> <p>All benchmarks were executed for SV-COMP 2024 <a href="https://sv-comp.sosy-lab.org/2024/">https://sv-comp.sosy-lab.org/2024/</a> by Dirk Beyer, LMU Munich, based on the following components:</p> <ul> <li><a href="https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks">https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks</a> svcomp24</li> <li><a href="https://gitlab.com/sosy-lab/sv-comp/bench-defs">https://gitlab.com/sosy-lab/sv-comp/bench-defs</a> svcomp24</li> <li><a href="https://github.com/sosy-lab/benchexec">https://github.com/sosy-lab/benchexec</a> 3.21</li> <li><a href="https://gitlab.com/sosy-lab/benchmarking/fm-tools">https://gitlab.com/sosy-lab/benchmarking/fm-tools</a> svcomp24</li> <li><a href="https://gitlab.com/sosy-lab/benchmarking/sv-witnesses">https://gitlab.com/sosy-lab/benchmarking/sv-witnesses</a> svcomp24</li> <li><a href="https://gitlab.com/sosy-lab/software/coveriteam">https://gitlab.com/sosy-lab/software/coveriteam</a> 1.1</li> <li><a href="https://gitlab.com/sosy-lab/benchmarking/competition-scripts">https://gitlab.com/sosy-lab/benchmarking/competition-scripts</a> svcomp24</li> </ul> <h2>Contact</h2> <p>Feel free to contact me in case of questions: <a href="https://www.sosy-lab.org/people/beyer/">https://www.sosy-lab.org/people/beyer/</a></p>
Replication Package: Pandemic Startup Software Engineering: An Experience Report on the Development of a COVID-19 Certificate Verification System
<p><strong>Welcome to the public repository for the additional content of the paper "Pandemic Startup Software Engineering: An Experience Report on the Development of a COVID-19 Certificate Verification System" (Journal of Systems and Software)<br></strong></p> <p>This repository provides additional information to the experience report, including the following files:</p> <ul> <li>survey_questions_de.txt: sheet containing the online questionnaire in German (original language)</li> <li>survey_questions_en.txt: sheet containing the online questionnaire translated into English</li> <li>survey_answers_original.csv: sheet containing the extracted questionnaire data of the participants in German (original language)</li> <li>survey_analysis.csv: sheet containing the analysis of the extracted questionnaire data in English</li> </ul>
Results of the 11th Intl. Competition on Software Verification (SV-COMP 2022)
<p>SV-COMP 2022</p> <p>Competition Results</p> <p>This file describes the contents of an archive of the 11th Competition on Software Verification (SV-COMP 2022).<br> <a href="https://sv-comp.sosy-lab.org/2022/">https://sv-comp.sosy-lab.org/2022/</a></p> <p>The competition was run by Dirk Beyer, LMU Munich, Germany.<br> More information is available in the following article:<br> Dirk Beyer. <em>Progress on Software Verification: SV-COMP 2022.</em> In Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022, Munich, April 2 - 7), 2022. Springer.</p> <p>Copyright (C) Dirk Beyer<br> <a href="https://www.sosy-lab.org/people/beyer/">https://www.sosy-lab.org/people/beyer/</a></p> <p>SPDX-License-Identifier: CC-BY-4.0<br> <a href="https://spdx.org/licenses/CC-BY-4.0.html">https://spdx.org/licenses/CC-BY-4.0.html</a></p> <p>To browse the competition results with a web browser, there are two options:</p> <ul> <li>start a local web server using php -S localhost:8000 in order to view the data in this archive, or</li> <li>browse <a href="https://sv-comp.sosy-lab.org/2022/results/">https://sv-comp.sosy-lab.org/2022/results/</a> in order to view the data on the SV-COMP web page.</li> </ul> <p>Contents</p> <ul> <li><code>index.html</code>: directs to the overview web page</li> <li><code>LICENSE.txt</code>: specifies the license</li> <li><code>README.txt</code>: this file</li> <li><code>results-validated/</code>: results of validation runs</li> <li><code>results-verified/</code>: results of verification runs and aggregated results</li> </ul> <p>The folder <code>results-validated/</code> contains the results from validation runs:</p> <ul> <li><code>*.xml.bz2</code>: XML results from BenchExec</li> <li><code>*.logfiles.zip</code>: output from tools</li> <li><code>*.json.gz</code>: mapping from files names to SHA 256 hashes for the file content</li> </ul> <p>The folder <code>results-verified/</code> contains the results from verification runs and aggregated results:</p> <ul> <li> <p><code>index.html</code>: overview web page with rankings and score table</p> </li> <li> <p><code>design.css</code>: HTML style definitions</p> </li> <li> <p><code>*.xml.bz2</code>: XML results from BenchExec</p> </li> <li> <p><code>*.merged.xml.bz2</code>: XML results from BenchExec, status adjusted according to the validation results</p> </li> <li> <p><code>*.logfiles.zip</code>: output from tools</p> </li> <li> <p><code>*.json.gz</code>: mapping from files names to SHA 256 hashes for the file content</p> </li> <li> <p><code>*.xml.bz2.table.html</code>: HTML views on the detailed results data as generated by BenchExec’s table generator</p> </li> <li> <p><code>*.All.table.html</code>: HTML views of the full benchmark set (all categories) for each tool</p> </li> <li> <p><code>META_*.table.html</code>: HTML views of the benchmark set for each meta category for each tool, and over all tools</p> </li> <li> <p><code><category>*.table.html</code>: HTML views of the benchmark set for each category over all tools</p> </li> <li> <p><code>iZeCa0gaey.html</code>: HTML views per tool</p> </li> <li> <p><code>validatorStatistics.html</code>: Statictics of the validator runs</p> </li> <li> <p><code>quantilePlot-*</code>: score-based quantile plots as visualization of the results</p> </li> <li> <p><code>quantilePlotShow.gp</code>: example Gnuplot script to generate a plot</p> </li> <li> <p><code>score*</code>: accumulated score results in various formats</p> </li> </ul> <p>The hashes of the file names (in the files <code>*.json.gz</code>) are useful for</p> <ul> <li>validating the exact contents of a file and</li> <li>accessing the files from the witness store.</li> </ul> <p>Other Archives</p> <p>Overview over archives from SV-COMP 2022 that are available at Zenodo:</p> <ul> <li><a href="https://doi.org/10.5281/zenodo.5831005">https://doi.org/10.5281/zenodo.</a><a href="https://doi.org/10.5281/zenodo.5838498">5838498</a> Verification Witnesses from SV-COMP 2022 Verification Tools. Witness store (containing the generated verification witnesses)</li> <li><a href="https://doi.org/10.5281/zenodo.5831008">https://doi.org/10.5281/zenodo.5831008</a> Results of the 11th Intl. Competition on Software Verification (SV-COMP 2022). Results (XML result files, log files, file mappings, HTML tables)</li> <li><a href="https://doi.org/10.5281/zenodo.5831003">https://doi.org/10.5281/zenodo.5831003</a> SV-Benchmarks: Benchmark Set of SV-COMP 2022 and Test-Comp 2022. Verification tasks, version svcomp22</li> <li><a href="https://doi.org/10.5281/zenodo.5720267">https://doi.org/10.5281/zenodo.5720267</a> BenchExec, version 3.10. Benchmarking framework</li> </ul> <p>All benchmarks were executed for SV-COMP 2022 <a href="https://sv-comp.sosy-lab.org/2022/">https://sv-comp.sosy-lab.org/2022/</a> by Dirk Beyer, LMU Munich, based on the following components:</p> <ul> <li><a href="https://gitlab.com/sosy-lab/sv-comp/archives-2022">https://gitlab.com/sosy-lab/sv-comp/archives-2022</a> svcomp22 a6b18082</li> <li><a href="https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks">https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks</a> svcomp22 ad265d07</li> <li><a href="https://gitlab.com/sosy-lab/sv-comp/bench-defs">https://gitlab.com/sosy-lab/sv-comp/bench-defs</a> svcomp22 0332884a</li> <li><a href="https://gitlab.com/sosy-lab/software/benchexec">https://gitlab.com/sosy-lab/software/benchexec</a> 3.10 4e8716bd</li> <li><a href="https://gitlab.com/sosy-lab/benchmarking/competition-scripts">https://gitlab.com/sosy-lab/benchmarking/competition-scripts</a> svcomp22 3c959671</li> <li><a href="https://github.com/sosy-lab/sv-witnesses">https://github.com/sosy-lab/sv-witnesses</a> svcomp22 e4695d2b</li> </ul> <p>Contact</p> <p>Feel free to contact me in case of questions: <a href="https://www.sosy-lab.org/people/beyer/">https://www.sosy-lab.org/people/beyer/</a></p>
Data and software from: Decomposition of skill scores for conditional verification – Impact of AMO phases on the predictability of decadal temperature forecasts
<p>Data and software from "Decomposition of skill scores for conditional verification – Impact of AMO phases on the predictability of decadal temperature forecasts"</p> <ul> <li>synthetic data and score computation routine</li> <li>data from MiKlip decadal prediction systems preop-dcpp-HR, preop-LR and observational HadCRUT4 data used for the conditional verification</li> <li>AMO calculation routine</li> <li>AMO data and phases defining the ocean state used in the conditional verification</li> </ul> <p>The computation routines from the conditional verification of decadal predcition systems is publicly available as the Freva plug-in "ProblEMS" at <a href="https://doi.org/10.5281/zenodo.10469658">https://doi.org/10.5281/zenodo.10469658</a></p> <p> </p>
Reproduction Package for FM 2024 Article `Software Verification with CPAchecker 3.0: Tutorial and User Guide'
<p>This package allows you to check the claims of our FM 2024 tutorial paper<br><em>Software Verification with CPAchecker 3.0: Tutorial and User Guide</em>.</p> <p>See the <strong>README.html</strong> for more information.</p> <p>Abstract:<br><em>This tutorial provides an introduction to CPAchecker for users. CPAchecker is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as BDDs, explicit values, intervals, memory graphs, and predicates, and many program-analysis and model-checking algorithms, such as abstract interpretation, bounded model checking, Impact, interpolation-based model checking, k-induction, PDR, predicate abstraction, and symbolic execution. This tutorial presents basic use cases for CPAchecker in formal software verification, focusing on its main verification techniques with their strengths and weaknesses. An extended version also shows further use cases of CPAchecker for test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge of CPAchecker is not required. This tutorial and user guide is based on CPAchecker in version 3.0. This user guide’s latest version and other documentation are available at <a href="https://cpachecker.sosy-lab.org/doc.php">https://cpachecker.sosy-lab.org/doc.php</a>.</em></p> <p> </p>
Replication Package - Moderator Factors of Software Security and Performance Verification
<p>Replication package for the paper "Moderator Factors of Software Security and Performance Verification"</p>
SV-Benchmarks: Benchmark Set for Software Verification and Testing (SV-COMP 2023 and Test-Comp 2023)
<p>Full benchmark set of the</p> <ul> <li>12th Intl. Competition on Software Verification (SV-COMP 2023) and the</li> <li>5th Intl. Competition on Software Testing (Test-Comp 2023).</li> </ul> <p>Licenses are included with the source code.</p>
Results of the 12th Intl. Competition on Software Verification (SV-COMP 2023)
<p><strong>SV-COMP 2023</strong></p> <p><strong>Competition Results</strong></p> <p>This file describes the contents of an archive of the 12th Competition on Software Verification (SV-COMP 2023). <a href="https://sv-comp.sosy-lab.org/2023/">https://sv-comp.sosy-lab.org/2023/</a></p> <p>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.</p> <p>Copyright (C) Dirk Beyer <a href="https://www.sosy-lab.org/people/beyer/">https://www.sosy-lab.org/people/beyer/</a></p> <p>SPDX-License-Identifier: CC-BY-4.0 <a href="https://spdx.org/licenses/CC-BY-4.0.html">https://spdx.org/licenses/CC-BY-4.0.html</a></p> <p>To browse the competition results with a web browser, there are two options:</p> <ul> <li>start a local web server using php -S localhost:8000 in order to view the data in this archive, or</li> <li>browse <a href="https://sv-comp.sosy-lab.org/2023/results/">https://sv-comp.sosy-lab.org/2023/results/</a> in order to view the data on the SV-COMP web page.</li> </ul> <p><strong>Contents</strong></p> <ul> <li><code>index.html</code>: directs to the overview web page of the verification track</li> <li><code>index-validation.html</code>: directs to the overview web page of the validation track</li> <li><code>LICENSE-results.txt</code>: specifies the license</li> <li><code>README-results.txt</code>: this file</li> <li><code>results-validated/</code>: results of validation runs</li> <li><code>results-verified/</code>: results of verification runs</li> </ul> <p>The folder <code>results-validated/</code> contains the results from validation runs:</p> <ul> <li> <p><code>index.html</code>: overview web page with rankings and score table</p> </li> <li> <p><code>design.css</code>: HTML style definitions</p> </li> <li> <p><code>*.results.txt</code>: TXT results from BenchExec</p> </li> <li> <p><code>*.xml.bz2</code>: XML results from BenchExec</p> </li> <li> <p><code>*.fixed.xml.bz2</code>: XML results from BenchExec, status adjusted according to the validation results</p> </li> <li> <p><code>*.logfiles.zip</code>: output from tools</p> </li> <li> <p><code>*.json.gz</code>: mapping from files names to SHA 256 hashes for the file content</p> </li> <li> <p><code><validator>*.table.html</code>: HTML views of the full benchmark set (all categories) for each validator</p> </li> <li> <p><code><category>*.table.html</code>: HTML views of the benchmark set for each category over all validators</p> </li> <li> <p><code>*.xml</code>: XML table definitions for the above tables</p> </li> <li> <p><code>validators.*</code>: Statistics of the validator runs (obsolete)</p> </li> <li> <p><code>.correctness.</code>: Infix for validation of correctness witnesses</p> </li> <li> <p><code>.violation.</code>: Infix for validation of violation witnesses</p> </li> <li> <p><code>quantilePlot-*</code>: score-based quantile plots as visualization of the results</p> </li> <li> <p><code>quantilePlotShow.gp</code>: example Gnuplot script to generate a plot</p> </li> <li> <p><code>score*</code>: accumulated score results in various formats</p> </li> </ul> <p>The folder <code>results-verified/</code> contains the results from verification runs and aggregated results:</p> <ul> <li> <p><code>index.html</code>: overview web page with rankings and score table</p> </li> <li> <p><code>design.css</code>: HTML style definitions</p> </li> <li> <p><code>*.results.txt</code>: TXT results from BenchExec</p> </li> <li> <p><code>*.xml.bz2</code>: XML results from BenchExec</p> </li> <li> <p><code>*.fixed.xml.bz2</code>: XML results from BenchExec, status adjusted according to the validation results</p> </li> <li> <p><code>*.logfiles.zip</code>: output from tools</p> </li> <li> <p><code>*.json.gz</code>: mapping from files names to SHA 256 hashes for the file content</p> </li> <li> <p><code>*.xml.bz2.table.html</code>: HTML views on the detailed results data as generated by BenchExec’s table generator</p> </li> <li> <p><code><verifier>*.table.html</code>: HTML views of the full benchmark set (all categories) for each verifier</p> </li> <li> <p><code>META_*.table.html</code>: HTML views of the benchmark set for each meta category for each verifier, and over all verifiers</p> </li> <li> <p><code><category>*.table.html</code>: HTML views of the benchmark set for each category over all verifiers</p> </li> <li> <p><code>*.xml</code>: XML table definitions for the above tables</p> </li> <li> <p><code>validatorStatistics.html</code>: Statistics of the validator runs (obsolete)</p> </li> <li> <p><code>results-per-tool.php</code>: List of results for each tool for review process in pre-run phase</p> </li> <li> <p><code><tool>.list.html</code>: List of results for a tool in HTML format with links</p> </li> <li> <p><code>quantilePlot-*</code>: score-based quantile plots as visualization of the results</p> </li> <li> <p><code>quantilePlotShow.gp</code>: example Gnuplot script to generate a plot</p> </li> <li> <p><code>score*</code>: accumulated score results in various formats</p> </li> </ul> <p>The hashes of the file names (in the files <code>*.json.gz</code>) are useful for</p> <ul> <li>validating the exact contents of a file and</li> <li>accessing the files from the witness store.</li> </ul> <p><strong>Other Archives</strong></p> <p>Overview over archives from SV-COMP 2023 that are available at Zenodo:</p> <ul> <li><a href="https://doi.org/10.5281/zenodo.7627791">https://doi.org/10.5281/zenodo.7627791</a> Verification Witnesses from SV-COMP 2023 Verification Tools. Witness store (containing the generated verification witnesses)</li> <li><a href="https://doi.org/10.5281/zenodo.7627829">https://doi.org/10.5281/zenodo.7627829</a> Tool Archives from SV-COMP 2023. Executable tools that were evaluated in the competition</li> <li><a href="https://doi.org/10.5281/zenodo.7627787">https://doi.org/10.5281/zenodo.7627787</a> Results of the 12th Intl. Competition on Software Verification (SV-COMP 2023). Results (XML result files, log files, file mappings, HTML tables)</li> <li><a href="https://doi.org/10.5281/zenodo.7627783">https://doi.org/10.5281/zenodo.7627783</a> SV-Benchmarks: Benchmark Set of SV-COMP 2023 and Test-Comp 2023. Verification tasks, version svcomp23</li> <li><a href="https://doi.org/10.5281/zenodo.7612021">https://doi.org/10.5281/zenodo.7612021</a> BenchExec, version 3.16. Benchmarking framework</li> </ul> <p>All benchmarks were executed for SV-COMP 2023 <a href="https://sv-comp.sosy-lab.org/2023/">https://sv-comp.sosy-lab.org/2023/</a> by Dirk Beyer, LMU Munich, based on the following components:</p> <ul> <li><a href="https://gitlab.com/sosy-lab/sv-comp/archives-2023">https://gitlab.com/sosy-lab/sv-comp/archives-2023</a> svcomp23 ca51c0c69ed4d4f6fd867c10abbc9b000d8ffb03</li> <li><a href="https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks">https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks</a> svcomp23 f87854c275a177e8dc3673fe6959cd89038652af</li> <li><a href="https://gitlab.com/sosy-lab/sv-comp/bench-defs">https://gitlab.com/sosy-lab/sv-comp/bench-defs</a> svcomp23 d34d04f1332a49c219293798b90eee6b3760946d</li> <li><a href="https://gitlab.com/sosy-lab/software/benchexec">https://gitlab.com/sosy-lab/software/benchexec</a> 3.16 b43e7384112770a41b571399135065daa7f387ab</li> <li><a href="https://gitlab.com/sosy-lab/benchmarking/competition-scripts">https://gitlab.com/sosy-lab/benchmarking/competition-scripts</a> svcomp23 e6f84b5a79626b4295108a0f96ea370edde1f023</li> <li><a href="https://github.com/sosy-lab/sv-witnesses">https://github.com/sosy-lab/sv-witnesses</a> svcomp23 e16b1fdddfa7770918c2d06bdcd0103e88e32691</li> <li><a href="https://gitlab.com/sosy-lab/software/coveriteam">https://gitlab.com/sosy-lab/software/coveriteam</a> svcomp23 76a8e4dba327af4606e2a30544656b7882f75848</li> </ul> <p><strong>Contact</strong></p> <p>Feel free to contact me in case of questions: <a href="https://www.sosy-lab.org/people/beyer/">https://www.sosy-lab.org/people/beyer/</a></p>
Korn—Software Verification with Horn clauses (Post-Competition Evaluation)
<p>Korn is a software verifier that infers correctness certificates automatically using state-of-the-art Horn-clause solvers, such as Z3 and Eldarica, which are used in a portfolio together with cheap random sampling. The tool is available at https://github.com/gernst/korn.</p> <p>This data documents the post SV-COMP 2023 experiments of Korn.</p>
Results of the 9th International Competition on Software Verification (SV-COMP 2020)
<p>This archive contains the results of the<br> 9th Competition on Software Verification (SV-COMP 2020)<br> https://sv-comp.sosy-lab.org/2020/</p> <p>The competition was run by Dirk Beyer, LMU Munich, Germany.</p> <p>Copyright (C) Dirk Beyer<br> https://www.sosy-lab.org/people/beyer/</p> <p>SPDX-License-Identifier: CC-BY-4.0<br> https://spdx.org/licenses/CC-BY-4.0.html</p> <p><br> To browse the competition results with a web browser, there are two options:<br> - start a local web server using<br> php -S localhost:8000<br> in order to view the data in this archive, or<br> - browse https://sv-comp.sosy-lab.org/2020/results/<br> in order to view the data on the SV-COMP web page.</p> <p><br> Contents:</p> <p>index.html directs to the overview web page<br> LICENSE.txt specifies the license<br> README.txt this file<br> results-validated/ results of validation runs<br> results-verified/ results of verification runs and aggregated results</p> <p><br> The folder results-validated/ contains the results from validation runs:</p> <p>- *.xml.bz2 XML results from BenchExec<br> - *.logfiles.zip output from tools<br> - *.json.gz mapping from files names to SHA 256 hashes for the file content</p> <p><br> The folder results-verified/ contains the results from verification runs and aggregated results:</p> <p>index.html overview web page with rankings and score table<br> *.xml.bz2 XML results from BenchExec<br> *.merged.xml.bz2 XML results from BenchExec, status adjusted according to the validation results<br> *.logfiles.zip output from tools<br> *.json.gz mapping from files names to SHA 256 hashes for the file content<br> *.xml.bz2.table.html HTML views on the detailed results data as generated by BenchExec's table generator<br> *.All.table.html HTML views of the full benchmark set (all categories) for each tool<br> META_*.table.html HTML views of the benchmark set for each meta category for each tool, and over all tools<br> <category>*.table.html HTML views of the benchmark set for each category over all tools<br> iZeCa0gaey.html HTML views per tool<br> validatorStatistics.html Statictics of the validator runs</p> <p>quantilePlot-* score-based quantile plots as visualization of the results<br> quantilePlotShow.gp example Gnuplot script to generate a plot<br> score* accumulated score results in various formats</p> <p><br> The hashes of the files (in the files *.json.gz) are useful for<br> - validating the exact contents of a file and<br> - accessing the files from the witness store.</p> <p>The witness store from SV-COMP 2020 is available at: https://doi.org/10.5281/zenodo.3630187<br> The verification tasks, version svcomp20, are available at: https://doi.org/10.5281/zenodo.3633334<br> BenchExec, version 2.5.1, is available at: https://doi.org/10.5281/zenodo.3574420</p> <p>All benchmarks were executed<br> for SV-COMP 2020, https://sv-comp.sosy-lab.org/2020/<br> by Dirk Beyer, LMU Munich<br> based on the components<br> git@github.com:sosy-lab/sv-benchmarks.git testcomp20-freeze-1-g2518814029<br> git@github.com:sosy-lab/sv-comp.git svcomp20<br> git@github.com:sosy-lab/benchexec.git 2.5</p> <p><br> Feel free to contact me in case of questions:<br> https://www.sosy-lab.org/people/beyer/</p> <p> </p>
SV-Benchmarks: Benchmark Set for Software Verification (SV-COMP 2024)
Open the record for dataset details and reuse information.
Formal verification of software architectures with SysADL Studio
<p>This short video demonstrates how to formally verify a software architecture description expressed in the <a href="https://sysadl.imd.ufrn.br">SysADL architectural language</a> using its supporting tool, SysADL Studio.</p>
ScienceDex guides
Understand access before you commit
These curated guides explain access requirements, typical timelines, costs, and reuse considerations for widely used research datasets.
Allen Brain Atlas
Allen Brain Atlas is an Allen Institute collection of brain map atlases, datasets, APIs, and analysis tools covering mouse, human, and non-human primate brain resources.
Annotated Behaviour and Observability Dataset (ABODe)
ABODe is a University of Edinburgh DataShare dataset for behavior classification in group-housed mice using home-cage video, identities, bounding boxes, ground-plate positions, and annotator labels.
DANDI Archive for NWB datasets
DANDI is a BRAIN Initiative archive for publishing and sharing neurophysiology data, including electrophysiology, optophysiology, and behavioral data packaged as NWB and related standards.
International Brain Laboratory public data
The International Brain Laboratory public data releases expose standardized mouse decision-making experiments, including Neuropixels recordings, widefield calcium imaging, behavior, and session metadata accessed through the ONE API.
OpenNeuro
OpenNeuro is a free, open platform for sharing neuroimaging datasets, with public search, dataset pages, and download paths for web, S3, DataLad, and the OpenNeuro CLI.