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.
7
datasets available to search
ShareScore release 0.9.0
Dataset results
7 results for “SMT-LIB”
TriCera Benchmarks: SMT-LIB Encodings of SV-COMP 2022 Benchmarks by TriCera
<p>This repository contains the SMT-LIB v2.6 encodings of a subset of SV-COMP 2022 benchmarks from the <em>reach-safety</em> and the <em>memsafety</em> categories, encoded by <a href="https://github.com/uuverifiers/tricera">TriCera</a> and <a href="https://github.com/zafer-esen/heap2array">heap2array</a> [1, 2]. The source benchmarks from SV-Comp 2022 (`.c` and `.i` files together with their accompanying `.yml` files) are not provided due to licensing reasons; the files are freely available for download at <a href="https://zenodo.org/record/5831003/export/hx">https://zenodo.org/record/5831003/export/hx</a></p> <p>- `benchmarks/heap` contains all heap benchmarks (encoded by TriCera using the <a href="https://arxiv.org/abs/2104.04224">theory of heaps</a>, used in [1] and [2]).<br> - `benchmarks/heap2array` contains all heap2array encoded benchmarks (encoded from heap benchmarks using heap2array, used in [1] and [2]).<br> - `benchmarks/nonHeapBms` contains all non-heap benchmarks (encoded by TriCera, used in [2]).</p> <p>[1] (to appear) Zafer Esen and Philipp Rümmer, "An SMT-LIB Theory of Heaps", SMT 2022<br> [2] (to appear) Zafer Esen and Philipp Rümmer, "TriCera: Verifying C Programs Using the Theory of Heaps", FMCAD 2022</p>
Dataset supporting the paper 'Integration of SMT-LIB Support into Maple'
<p>This dataset provides a listing of all distinct queries to the Maple commands <strong>is</strong> and <strong>coulditbe </strong>which occurred in the course of a complete run through the Maple library test suite using Maple 2017 on 26 July 2017. The results include:</p> <ul> <li>24085 distinct queries to <strong>is</strong> (which tests if a given proposition holds universally) - see file is_queries.txt</li> <li>5771 distinct queries to <strong>coulditbe</strong> (which tests if given proposition is satisfiable) - see file coulditbe_queries.txt</li> </ul> <p>The files are plaintext and each line corresponds to a distinct query. Queries are in Maple syntax and adhere to one of the following patterns:</p> <ul> <li><strong>coulditbe(</strong><em>X</em><strong>)</strong></li> <li><strong>coulditbe(</strong><em>X</em><strong>) assuming </strong><em>Y</em></li> <li><strong>is(</strong><em>X</em><strong>)</strong></li> <li><strong>is(</strong><em>X</em><strong>) assuming </strong><em>Y</em></li> </ul> <p>Here, <em>X</em> is the expression being tested (in Maple syntax) and <em>Y</em> is an expression sequence of one or more assumptions on symbols appearing in <em>X</em>.</p> <ul> </ul>
SMT-LIB release 2023 (non-incremental benchmarks)
<p>This is the SMT-LIB benchmark library: a large library of input problems, or benchmarks, written in the SMT-LIB language. More information about the SMT-LIB initiative can be found at <a href="https://smtlib.cs.uiowa.edu/">https://smtlib.cs.uiowa.edu/</a>. The contributor and licence of each benchmark is indicated in the metadata fields of each benchmark file.</p> <p>This collection contains the <strong>non-incremental benchmarks</strong>.</p> <p>Benchmarks are grouped by logic and compressed with the <code>zstd</code> compression algorithm using the <code>tar --zstd</code>. SMT-LIB benchmarks usually have a very high compression rate, be aware of the required disk space when uncompressing the archives. You can find the size of each archive in compressed and uncompressed form in the following list.</p>
SMT-LIB release 2023 (incremental benchmarks)
<p>This is the SMT-LIB benchmark library: a large library of input problems, or benchmarks, written in the SMT-LIB language. More information about the SMT-LIB initiative can be found at <a href="https://smtlib.cs.uiowa.edu/">https://smtlib.cs.uiowa.edu/</a>. The contributor and licence of each benchmark is indicated in the metadata fields of each benchmark file.</p> <p>This collection contains the <strong>incremental benchmarks</strong>.</p> <p>Benchmarks are grouped by logic and compressed with the <code>zstd</code> compression algorithm using the <code>tar --zstd</code>. SMT-LIB benchmarks usually have a very high compression rate, be aware of the required disk space when uncompressing the archives. You can find the size of each archive in compressed and uncompressed form in the following list.</p>
Benchmarks from the paper titled "An SMT-LIB Theory of Heaps" submtted to SMT 2022
<p>Benchmarks from the paper titled "An SMT-LIB Theory of Heaps" submtted to SMT 2022</p> <p><strong>benchmarks/</strong><br> This directory contains all benchmarks (excluding SV-Comp sources).<br> - <strong>benchmarks/heap</strong> contains all heap benchmarks (smt2). <br> - <strong>benchmarks/heap2array</strong> contains all heap2array encoded benchmarks (smt2).</p> <p>The source benchmarks from SV-Comp 2022 (`.c` and `.i` files together with their accompanying `.yml` files) are not provided in this repository due to licensing reasons, but the files are freely available for download: <a href="https://zenodo.org/record/5831003/export/hx">https://zenodo.org/record/5831003/export/hx</a></p>
SMT-LIB release 2024 (non-incremental benchmarks)
<p>This is the SMT-LIB benchmark library: a large library of input problems, or benchmarks, written in the SMT-LIB language. More information about the SMT-LIB initiative can be found at <a href="https://smt-lib.org">https://smt-lib.org</a>. The contributor and licence of each benchmark is indicated in the metadata fields of each benchmark file.</p> <p>This collection contains the <strong>non-incremental benchmarks</strong>.</p> <p>Benchmarks are grouped by logic and compressed with the <code>zstd</code> compression algorithm using the <code>tar --zstd</code>. SMT-LIB benchmarks usually have a very high compression rate, be aware of the required disk space when uncompressing the archives. You can find the size of each archive in compressed and uncompressed form in the following list.</p>
SMT-LIB release 2024 (incremental benchmarks)
<p>This is the SMT-LIB benchmark library: a large library of input problems, or benchmarks, written in the SMT-LIB language. More information about the SMT-LIB initiative can be found at <a href="https://smt-lib.org">https://smt-lib.org</a>. The contributor and licence of each benchmark is indicated in the metadata fields of each benchmark file.</p> <p>This collection contains the <strong>incremental benchmarks</strong>.</p> <p>Benchmarks are grouped by logic and compressed with the <code>zstd</code> compression algorithm using the <code>tar --zstd</code>. SMT-LIB benchmarks usually have a very high compression rate, be aware of the required disk space when uncompressing the archives. You can find the size of each archive in compressed and uncompressed form in the following list.</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.