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.
3
datasets available to search
ShareScore release 0.9.0
Dataset results
3 results for “SMT Formula”
SMT Formulas for Boolean Programs from SLAM
<p>This archive contains SMT formulas for boolean programs that were generated with the software verifier SLAM.</p> <p>The archive was contributed to the SV-Benchmarks repository (when it was still hosted as SVN repository) by Nikolaj Bjorner on Nov. 21, 2012. [https://github.com/sosy-lab/sv-benchmarks/commit/9a1394fe44b97c1fe8eeaea831a3627e34eb1c11]</p> <p>It is not contained directly in the Git repository at https://github.com/sosy-lab/sv-benchmarks/ because GitHub does not support files larger than 200 MB.</p>
Artifacts for Fuzzing SMT Solvers with Diversified Sub-formulas
<p><strong>Fuzzing SMT solvers with Diversified Sub-formulas</strong></p> <p>Table of Contents</p> <ul> <li>Background</li> <li>Install</li> <li>Usage</li> <li>Bugs</li> </ul> <p> </p> <p><strong>Background</strong></p> <p><strong>Octopus </strong>is the tool for detecting soundness bugs in SMT solvers. <br> We have submitted 10 valid bug reports for Z3 so far. 7 bugs are confirmed/fixed by developers among these reports.</p> <p> </p> <p><strong>Install</strong></p> <p>Octopus itself has few dependencies. It uses Python3 and Python-virtualenv.</p> <p>You can install Python-virtualenv using <code>pip install virtualenv</code></p> <p>Then install Octopus.</p> <p><code>virtualenv --python=/usr/bin/python3.6 virenv</code></p> <p><code>source virenv/bin/activate</code></p> <p><code>cd octopus</code></p> <p><code>python3 setup.py install</code> </p> <p> </p> <p><strong>Usage</strong></p> <p>You can download SMT instances in SMT COMP 2021 as benchmarks.</p> <p><a href="https://www.starexec.org/starexec/secure/explore/spaces.jsp?id=1">2021-05-26 - StarExec</a></p> <p>Then install and build the SMT solver you want to test.</p> <p>For example:</p> <p><code>git clone https://github.com/Z3Prover/z3.git</code></p> <p><code>python scripts/mk_make.py </code></p> <p><code>cd build; make</code></p> <p>Then Octopus can be used to validate it, for example:</p> <p><code>octopus --benchmark=/home/SMT2021 --solver=z3 --solverbin=../z3/build/z3 --theory=LIA</code></p> <p>To run Octopus in multiple cores:</p> <p><code>octopus --benchmark=/home/SMT2021 --solver=z3 --solverbin=../z3/build/z3 --theory=LIA --cores=20</code></p> <p> </p> <p><strong>Bugs</strong></p> <p>Octopus has detected many new refutational soundness bugs in Z3.</p> <p>Here is a list of issues we reported.</p> <p><a href="https://github.com/Z3Prover/z3/issues/5373">https://github.com/Z3Prover/z3/issues/5373</a> [confirmed]<br> <a href="https://github.com/Z3Prover/z3/issues/5443">https://github.com/Z3Prover/z3/issues/5443</a> [reported]<br> <a href="https://github.com/Z3Prover/z3/issues/5447">https://github.com/Z3Prover/z3/issues/5447</a> [fixed]<br> <a href="https://github.com/Z3Prover/z3/issues/5456">https://github.com/Z3Prover/z3/issues/5456</a> [fixed]<br> <a href="https://github.com/Z3Prover/z3/issues/5457">https://github.com/Z3Prover/z3/issues/5457</a> [fixed] <br> <a href="https://github.com/Z3Prover/z3/issues/5460">https://github.com/Z3Prover/z3/issues/5460</a> [fixed]<br> <a href="https://github.com/Z3Prover/z3/issues/5468">https://github.com/Z3Prover/z3/issues/5468</a> [fixed] <br> <a href="https://github.com/Z3Prover/z3/issues/5488">https://github.com/Z3Prover/z3/issues/5488</a> [fixed]<br> <a href="https://github.com/Z3Prover/z3/issues/5502">https://github.com/Z3Prover/z3/issues/5502</a> [duplicate]<br> <a href="https://github.com/Z3Prover/z3/issues/5508">https://github.com/Z3Prover/z3/issues/5508</a> [reported]<br> <a href="https://github.com/Z3Prover/z3/issues/5423">https://github.com/Z3Prover/z3/issues/5423</a> [invalid] </p>
Artifacts for Fuzzing SMT Solvers with Diversified Sub-formulas
<p>## Installation:<br> ```<br> virtualenv --python=/usr/bin/python3 virenv<br> source virenv/bin/activate<br> cd octopus<br> python3 setup.py install<br> ```</p> <p>## Usage:</p> <p>```<br> octopus --benchmark=[PATH TO SEED DIRECTORY] --solverbin=[PATH TO SOLVER BIN] --solver=[SOLVER NAME] --theory=[SOLVER THEORY]<br> ```</p> <p>For example:</p> <p>```<br> octopus --benchmark=/home/SMT2021 --solverbin=../z3/build/z3 --solver=z3 --theory=LIA<br> ```</p> <p>To run `n` parallel instances of octopus on `n` cores, use the `--cores` flag. For example:</p> <p>```<br> octopus --benchmark=[PATH TO SEED FILES] --solverbin=[PATH TO SOLVER BIN] --solver=[SOLVER NAME] --theory=LIA --cores=10<br> ```</p> <p><br> ## Refutational soundness bugs detected so far:<br> octopus has detected many new "refutational soundness" bugs in Z3. <br> Here is a list of issues we reported.</p> <p>https://github.com/Z3Prover/z3/issues/5373 `[z3]` `[QF_NRA]` <br><br> https://github.com/Z3Prover/z3/issues/5443 `[z3]` `[QF_BVFP]` <br><br> https://github.com/Z3Prover/z3/issues/5447 `[z3]` `[QF_ABV]` <br><br> https://github.com/Z3Prover/z3/issues/5456 `[z3]` `[QF_IDL]` <br><br> https://github.com/Z3Prover/z3/issues/5457 `[z3]` `[QF_BV]` <br><br> https://github.com/Z3Prover/z3/issues/5460 `[z3]` `[QF_BV]` <br><br> https://github.com/Z3Prover/z3/issues/5468 `[z3]` `[AUFLIRA]` <br><br> https://github.com/Z3Prover/z3/issues/5488 `[z3]` `[QF_BV]` <br><br> https://github.com/Z3Prover/z3/issues/5502 `[z3]` `[QF_NIA]` <br><br> https://github.com/Z3Prover/z3/issues/5508 `[z3]` `[QF_NIA]` <br><br> https://github.com/Z3Prover/z3/issues/5423 `[z3]` `[QF_BVFP]` `Won't fixed` <br><br> </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.