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.
412
datasets available to search
ShareScore release 0.9.0
Dataset results
412 results for “Verification”
Dataset for Validation of a Qualification Procedure Applied to the Verification of Partial Discharge Analysers Used for HVDC or HVAC Networks
<p>Data set for the publication named: "Validation of a Qualification Procedure Applied to the Verification of Partial Discharge Analysers Used for HVDC or HVAC Networks"</p>
Data from: Empirical verification of feeding selectivity of larval and juvenile pelagic fishes using in situ zooplankton communities
Open the record for dataset details and reuse information.
Experimental Verification of Nonlinear Effects in Peak Limiting Current Mode Controlled Boost Converter
<p>Compressed file contains results of experimental verification of nonlinear effects in peak limiting current mode controlled boost converter. Circuit diagrams are given in files <strong>power.pdf</strong> and <strong>control.pdf</strong> in the root directory. Directories</p> <p><strong>M-2019-05-02-8kHz-12V</strong></p> <p><strong>M-2019-05-02-8kHz-17V</strong></p> <p><strong>M-2019-05-02-8kHz-24V</strong></p> <p><strong>M-2019-05-02-8kHz-29V</strong></p> <p>contain the experimental results for Vout=12V, Vout=17V, Vout=24V, and Vout=29V. Each directory contains .npy files with numerical data, figures recorded by the oscilloscope, figure that depicts measured output current of the converter as it depends on the assigned control voltage, and programs that controlled the measurements. Out of 15009 files in each directory 15003 files are oscilloscope recordings, <strong>Iout.npy</strong> contains measured output current data, <strong>Vg.npy</strong> contains assigned control voltage data, <strong>figure.py</strong> is a Python 2 program used to plot Iout(Vg), which is stored in <strong>figure-xy.pdf</strong> (xy stands for the actual output voltage), while <strong>oscusb.py</strong> and <strong>overjm.py</strong> are programs used to control the experiment. Experiments are controlled by a computer running under GNU/Linux operating system.</p>
NEMO, HIDRA and Tide Gauge Datasets for HIDRA Machine Learning Algorithm Verification
<p>Supporting sea level datasets for paper:</p> <p>"HIDRA 1.0: Deep-Learning-Based Ensemble Sea Level Forecastingin the Northern Adriatic"</p> <p>by Lojze Žust, Anja Fettich, Matej Kristan, and Matjaž Ličer</p>
Policy Verification Using Metagraphs
<p>Code for the submission Policy Verification Using Metagraphs</p>
Towards the formal verification of data-intensive applications through metric temporal logic
p>The dataset consists of a set of model descriptions representingnbsp;span>Storm topologies. It is designed on purpose to show the approach presented in the paper quot;/span>span>Towards the formal verification of data-intensive applications through m/span>span>etric/span>span>nbsp;temporalnbsp;/span>span>logicquot; (F. Marconi, M.M. Bersani, M. Erascu and M. Rossi) which focuses on the analysisnbsp;/span>span>of bottleneck nodes of data intensive applications implemented with Storm./span>/p>
Dataset for Verification and Validation Tests of the Spalart-Allmaras Model in Moltres
<p>This repository contains input files, raw output data, data analysis scripts, and plots for verification and validation tests of the Spalart-Allmaras turbulence model in Moltres. These V&V tests consist of numerical simulations of turbulent channel, pipe, and backward-facing step flows based on the works by Moser et al. (1999), Laufer (1954), and Driver & Seegmiller (1985), respectively.</p>
High resolution wind speed measurements with multicopters of the SWUF-3D UAS fleet - calibration and verification in a wind tunnel with active grid
<p>This dataset contains aggregated measurements from multicopter UAS. The data were measured during the period from October 5, 2022 to October 12, 2022 in the ForWind wind tunnel at the University of Oldenburg with UAS of the SWUF-3D fleet against Constant Temperature Anemometer (CTA). </p><p>Recorded data are provided for measurement flights in different generated wind profiles, i.e. staircase profiles, gusts, velocity steps and statistical turbulence. The measurement data consist of the accelerations measured by the UAS in its longitudinal and lateral axes, as well as the wind speeds measured by the CTA. The latter data were sampled down to the sampling rate of the UAS wind measurement. For the measurements in statistical turbulence, additional files are provided which contain the wind speeds measured by the CTA in its original sampling rate. Each file contains the data for a single measurement flight, as well as information in the header about the ambient conditions in the wind tunnel. The file names contain the following metadata:</p><p>for "gust" files:</p><ul><li>V0 : inertial velocity [m/s]</li><li>V_g : gust velocity amplitude [m/s]</li></ul><p>for "staircase" files:</p><ul><li>uas : the ID of the UAS used [-]</li><li>heading : yaw angle of UAS in relation to longitudinal axes of wind tunnel</li></ul><p>for "turbulence" files:</p><ul><li>V0 : fan wind speed [m/s]</li><li>I : turbulence intensity [%]</li><li>f_cta : sampling frequency of reference sensor [Hz] (for files with original sampling rate)</li></ul><p>for "velocity step" files:</p><ul><li>V0 : lower wind speed</li><li>V_du : wind speed aimed for of upward and downward velocity step</li></ul><p>All filenames end with the test date in YYYY-MM-DD format.</p>
Detailed Controller Synthesis and Laboratory Verification of a Matching-Controlled Grid-Forming Inverter for Microgrid Applications
<p><strong>Figure5 Blackstart:</strong><br>BS->blackstart<br>noload/min/inter->Initial load<br>U4 -> Voltage waveforms<br>Udq-> Voltage dq values</p> <p><strong>Figure6 Stat<br></strong>data_sati_voltage3 -> Current and voltage waveforms<br>THD -> THD values<br><br><strong>Figure7 Trans:</strong></p> <p>Trans4to7kwdq-> dq values<br>Trans4to7kwPower->P and Q values<br>Trans4to7kwUI->Waveforms</p> <p><strong>Figure8 DCSens:</strong><br>Test1-14 -> Tests corresponding to DC bus sensitivity<br>p/i min/max -> identifier wether p or i value were increased/decreased</p> <p><strong>Figure9 ACsens:</strong><br>AC0-22 -> Tests corresponding to AC sensitivity</p> <p> </p>
Verification Witnesses from Verification Tools (SV-COMP 2024)
<h1>SV-COMP 2024</h1> <h2>Verification Witnesses</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> <h2>Contents</h2> <ul> <li><code>LICENSE.txt</code>: specifies the license</li> <li><code>README.txt</code>: this file</li> <li><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 or .yml. The format of the verification witnesses is described on the format web page: <a href="https://github.com/sosy-lab/sv-witnesses/">https://github.com/sosy-lab/sv-witnesses/</a> A verification witness contains also metadata in order to relate it to the verification task for which it was produced.</li> <li><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.</li> <li><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.</li> </ul> <p>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. <a href="https://doi.org/10.1109/MSR.2019.00026">https://doi.org/10.1109/MSR.2019.00026</a></p> <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>
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>
Verification of ORM-based Controllers by Summary Inference
<p>The folder structure in icse2022-subm-data-1008-orm-verification is as follows:</p> <p>ControllerVerificationData contains results corresponding to Section 5.2 of<br> the paper. The folder hierarchy within this is:</p> <p> benchmark name -></p> <p> Controller class name -></p> <p> "Alloy" -></p> <p> a .als file (i.e., Alloy model/summary generated by our tool)<br> corresponding to each controller method, with assertions added<br> manually in all cases were they were expressible.</p> <p> "Output" -> outputs from Alloy for the assertions.</p> <p>multipage-data contains results corresponding to Section 5.3 of the paper.</p> <p> "properties" -></p> <p> each .txt file contains a property (basically, a \psi as in Section<br> 3.1 in the paper), written by us, in Alloy form. (For "Unexpressed"<br> properties, we wrote a dummy property.)</p> <p> "toCheck" -></p> <p> a property number -></p> <p> Generated Alloy files for this property (one Alloy file for Property<br> (A) and one each for Property (I), see Section 3.1 in the paper)</p> <p> A .txt file for each Alloy file, containing Alloy checker's output.</p> <p> "summary.txt" contains a summary of all the information above</p> <p>Mutation-Analysis contains results corresponding to Section 5.5 of the<br> paper.</p> <p> Each leaf level folder under this contains:</p> <p> Alloy file generated for a mutated version of the benchmark, with<br> assertions added manually.</p> <p> The description of the mutation (in the .desc file)</p> <p> A .out file containing output from the Alloy checker for the assertions<br> in the .als file. </p> <p>JPF contains results corresponding to Section 5.6 of the paper. </p> <p> Each leaf-level folder contains results pertaining to one of the 16<br> assertions. The .java file contains a driver that initializes the tables,<br> calls the controller, and checks the assertion. The .jpf file is required<br> by JPF, and the .out file shows the JPF output. </p> <p>The structure of folder src/ is as follows:<br> -ControllerSummaryInference-src: Code for inferring relational-algebraic summaries of Spring-based web applications and alloy translation.<br> -multipage-src: Code for checking trace properties.<br> </p> <p>The file other-details.pdf contains syntax directed rules as well as loop patterns in tool which form the approach to infer</p> <p>relational summaries from ORM controllers.</p>
Verification of some Boolean partial polymorphisms
<p>This dataset contains the formal verification that a certain partial ternary Boolean conjunction <em>f</em> preserves two specific Boolean relations, but does not preserve two other ones. Our approach is by translating the question into Boolean satisfiability problems and to implement these such that they can be treated by a sat solver being capable of reading SMT-LIB2.0 specifications. Specifically, we have been using the Z3 solver developed by Microsoft Research (https://github.com/z3prover/z3) to attack the problem. The following is a list of the files contained in the dataset and their function:</p> <table> <tbody><tr> <th>Filename</th> <th>Purpose</th> </tr> </tbody><tbody> <tr> <td>f-pPol-GammaL0chi2-GammaL2chi3.<br> z3</td> <td>The SMT-LIB2.0 implementation of the problem, to be run, e.g. by Z3.</td> </tr> <tr> <td>z3-output.txt</td> <td>The output received by running Z3 on f-pPol-GammaL0chi2-GammaL2chi3.<br> z3</td> </tr> <tr> <td>f-preserves-GammaL0chi2_proof.txt</td> <td>A formal proof generated by Z3 that <em>f</em> preserves Γ<sub>L₀</sub>(χ₂).</td> </tr> <tr> <td>f-preserves-GammaL2chi3_proof.txt</td> <td>A formal proof generated by Z3 that <em>f</em> preserves Γ<sub>L₂</sub>(χ₃).</td> </tr> <tr> <td>partial_polymorphisms.pdf</td> <td>A detailed description of the problem and the dataset.</td> </tr> <tr> <td>partial_polymorphisms.tex</td> <td>The source file used to produce partial_polymorphisms.pdf</td> </tr> </tbody> </table> <p> </p>
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>
Verification Witnesses from Verification Tools (SV-COMP 2022)
<p>SV-COMP 2022</p> <p>Verification Witnesses</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>Contents</p> <ul> <li><code>LICENSE.txt</code>: specifies the license</li> <li><code>README.txt</code>: this file</li> <li><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: <a href="https://github.com/sosy-lab/sv-witnesses/">https://github.com/sosy-lab/sv-witnesses/</a> A verification witness contains also metadata in order to relate it to the verification task for which it was produced.</li> <li><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.</li> <li><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.</li> </ul> <p>The data structure is described in the following article:<br> 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.<br> <a href="https://doi.org/10.1109/MSR.2019.00026">https://doi.org/10.1109/MSR.2019.00026</a></p> <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="http://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><br> 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>
FaVCI2D Face Verification with Challenging Imposters and Diversified Demographics
<p>Face verification aims to distinguish between genuine and imposter pairs of faces, which include the same or different identities, respectively. The performance reported in recent years gives the impression that the task is practically solved. Here, we revisit the problem and argue that existing evaluation datasets were built using two oversimplifying design choices. First, the usual identity selection to form imposter pairs is not challenging enough because, in practice, verification is needed to detect challenging imposters. Second, the underlying demographics of existing datasets are often insufficient to account for the wide diversity of facial characteristics of people from across the world. To mitigate these limitations, we introduce the FaVCI2D dataset. Imposter pairs are challenging because they include visually similar faces selected from a large pool of demographically diversified identities. The dataset also includes metadata related to gender, country and age to facilitate fine-grained analysis of results. FaVCI2D is generated from freely distributable resources. Experiments with state-of-the-art deep models that provide nearly 100% performance on existing datasets show a significant performance drop for FaVCI2D, confirming our starting hypothesis. Equally important, we analyze legal and ethical challenges which appeared in recent years and hindered the development of face analysis research. We introduce a series of design choices which address these challenges and make the dataset constitution and usage more sustainable and fairer. FaVCI2D is available at https://github.com/AIMultimediaLab/FaVCI2D-Face-Verification-with-Challenging-Imposters-and-Diversified-Demographics</p>
[dataset] Runtime Equilibrium Verification for Resilient Cyber-physical Systems
<p>This package contains the <strong>raw data</strong> and <strong>scripts</strong> used to carry out the evaluation of the framework RUNE<sup>2</sup> (RUNtime Equilibrium verification and Enforcement).</p> <p>This package is paired with the following paper submitted for publication to the ACM Transactions on Autonomous and Adaptive Systems (TAAS). Invited contribution to the IEEE ACSOS 2021 Special Issue.</p> <p><strong>Title</strong>: Enforcing Resilience in Cyber-physical Systems via Equilibrium Verification at Runtime</p> <p><strong>Authors</strong>:<br> - Matteo Camilli, Free University of Bozen-Bolzano, Italy<br> - Raffaela Mirandola, Politecnico di Milano, Italy<br> - Patrizia Scandurra, University of Bergamo, Italy</p> <p>See README.md for further instructions.</p>
Dataset for publication: "Design and Verification of a Calculable Composite Voltage Calibrator"
<p>Dataset for publication: "Design and Verification of a Calculable Composite Voltage Calibrator". Excel file contains the data for Figures 5, 8, and 9.</p>
Raw Data to 'Experimental verification of the area law of mutual information in quantum field theory', arXiv:2206.10563
<p><strong>Absorption images representing the raw data for arXiv:2206.10563</strong></p> <p>'scan5722.zip' contains the raw data for figures 2 and 3.</p> <p>'scan5831.zip' and 'scan9617.zip' contain the raw data for figure 5, right and left, respectively.</p> <p>All three datasets, 9617, 5722, and 5831, are used to obtain the data points in figure 4, from low to high temperatures.</p> <p> </p> <p><strong>Scans 5722 & 5831</strong></p> <p>The absorption images are numbered consecutively.</p> <p>The first image for scans 5722 and 5831 is taken along the axial (longitudinal) direction with our 'longitudinal' imaging system after 10 ms time of flight (TOF) to measure the atom number balance between the two wells. The measurement is performed before ramping up the DW barrier. Two images are taken in each cycle: One shot with atoms ('1-atomcloud.tif') and a second image to record the intensity of the imaging beam without atoms ('1-withoutatoms.tif'). These two pictures are used to extract the atomic density (see the Matlab script).</p> <p>The second image for scans 5722 and 5831 is taken in the direction of the double-well (DW) separation with our 'transverse' imaging system. The measurement is performed before ramping up the DW barrier. The image is taken after 11.2 ms TOF.</p> <p>The subsequent images record the interference fringes for the different evolution times (again, always pairs '-atomcloud.tif' and '-withoutatoms.tif'). They are taken with our 'vertical' imaging system after 15.6 ms TOF. The imaging direction is perpendicular to the weakly confined direction of the clouds and the DW separation.</p> <p>The recorded evolution times for scan 5722 are -1.9 ms (right before ramping up the DW barrier), 0 ms (right after the DW barrier is ramped up), and then in steps of 2.5 ms until 65 ms. This means that '3-atomcloud.tif' corresponds to -1.9 ms, and '30-atomcloud.tif' corresponds to 65 ms. This completes the 'first repeat'. The next two shots, '31-atomcloud.tif' and '32-atomcloud.tif', belong to the 'second repeat' and are again taken with the 'longitudinal' & 'transverse' imaging systems, respectively. The picture '33-atomcloud.tif' is again taken with the 'vertical' imaging and corresponds to -1.9 ms. And so forth.</p> <p>In the same way, the pictures scan 5831 are ordered. The evolution times (in ms) for these two scans are:</p> <p>scan 5722: -1.9 from 0 to 65 (in steps of 2.5)</p> <p>scan 5831: -1.8, from 0 to 65 (in steps of 2.5)</p> <p>The first time always corresponds to the instant right before the DW barrier is ramped up. 0 is always right after the barrier was ramped up.</p> <p> </p> <p><strong>Scan 9617</strong></p> <p>This scan only contains images with the 'vertical' imaging system with 15.6 ms TOF. The evolution times (in ms) are as follows:</p> <p>scan 9617: -2.8, from 0 to 15 (in steps of 1.5), 22, 25, 28</p> <p>The first time always corresponds to the instant right before the DW barrier is ramped up. 0 is always right after the barrier was ramped up.</p> <p>This means, that '1-atomcloud.tif', '16-atomcloud.tif', '31-atomcloud.tif' and so on correspond to -2.8 ms, and '15-atomcloud.tif', '30-atomcloud.tif', '45-atomcloud.tif' and so on correspond to 28 ms.</p> <p> </p> <p><strong>Matlab script</strong></p> <p>In addition to the data, a Matlab script (calc_atomic_density.m) illustrates how to extract the two-dimensional atomic density from the absorption images. It contains all relevant parameters of the imaging systems.</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.