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.
52
datasets available to search
ShareScore release 0.9.0
Dataset results
52 results for “SMT”
IDMT-SMT-Bass Dataset
<p>The IDMT-SMT-Bass database is a large database for automatic bass transcription and signal processing.</p> <p>The overall duration of the audio material is approx. 3.6 hours.</p> <p>The dataset consists of approx. 4300 WAV files (44.1 kHz, 24bit) with single recorded notes.</p> <p>Overall, 10 different bass-related playing techniques namely 5 plucking styles</p> <ul> <li>fingerstyle (FS)</li> <li>picked (PK)</li> <li>muted (MU)</li> <li>slap-thumb (ST)</li> <li>slap-pluck (SP)</li> </ul> <p>and 5 expression styles</p> <ul> <li>normal (NO)</li> <li>vibrato (VI)</li> <li>bending (BE)</li> <li>harmonics (HA)</li> <li>dead-note (DN)</li> </ul> <p>are incorporated. A further explaination of the playing techniques is provided in</p> <blockquote> <p>Abeßer, Jakob; Lukashevich, Hanna; Schuller, Gerald: Feature-based extraction of plucking and expression styles of the electric bass guitar, Proceedings of the IEEE International Conference on Acoustics, Speech, and Signal Processing (ICASSP), 2010</p> </blockquote> <p>For each of the three expression techniques (vibrato, bending, slide), two subclasses were defined in:</p> <blockquote> <p>Abesser, Jakob; Dittmar, Christian; Schuller, Gerald: Automatic Recognition and Parametrization of Frequency Modulation Techniques in Bass-Guitar Recordings, Proceedings of the 42nd AES Conference on Semantic Audio 2011, Ilmenau, Germany</p> </blockquote> <ul> <li>fast vibrato, slow vibrato</li> <li>semi-tone bending, quarter-note bending</li> <li>slide up, slide down (recorded with fretless bass guitar)</li> </ul> <p>3 different 4-string electric bass guitars, each with 3 different pick-up settings were used for recording.<br> </p> <p>The notes cover the common pitch range of a 4-string bass guitar from E1 (41.2 Hz) to G3 (196.0 Hz).</p>
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>
Cadir Hoyuk SMT 16
Trench SMT 16 Source: Objaverse 1.0 / Sketchfab
Symbolic Automatic Relations and Their Applications to SMT and CHC Solving
<p>This is a replication package for the paper "Symbolic Automatic Relations and Their Applications to SMT and CHC Solving," published in the proceedings of the 28th Static Analysis Symposium (SAS 2021).</p> <p>This package contains all the tools discussed in the paper, and all the benchmarks the evaluation was conducted on, along with README.md and benchmark scripts.</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>
Dataset and Model Files for the Paper "Concrete Type Inference for Code Optimization using Machine Learning with SMT Solving"
<p>Dataset and model files for the paper "Concrete Type Inference for Code Optimization using Machine Learning with SMT Solving".</p>
fast-SMT movies of H2B-Halo neurons
<p>Fast single molecule tracking experiments performed on primary cortical neurons infected with a lentiviral vector expressing Halo-tagged H2B.</p>
fast-SMT movies of WT-MeCP2-Halo neurons
<p>Fast single molecule tracking experiments performed on primary cortical neurons with a wild type Mecp2 allele endogenously tagged with a HaloTag.</p>
fast-SMT movies of Halo-NLS neurons
<p>Fast single molecule tracking experiments performed on primary cortical neurons infected with a lentiviral vector expressing Halo-tagged NLS.</p>
fast-SMT movies of G118E-MeCP2-Halo neurons
<p>Fast single molecule tracking experiments performed on primary cortical neurons with a G118E Mecp2 allele endogenously tagged with a HaloTag.</p>
Benchmark files for thesis 'Extending the Framework JavaSMT with the SMT Solver Bitwuzla and Evaluation using CPAchecker'
Open the record for dataset details and reuse information.
Standard Maintenance Therapy (SMT) vs Local Consolidative Radiation Therapy and SMT in OM-NSCLC
ClinicalTrials.gov study NCT05278052. IPD Sharing: NO. Countries: 1. Publications: 1.
Sofusa System With Sumatriptan (KC5010) Phase 1 Dose Escalation Safety and PK Study (KCC-SMT-002)
ClinicalTrials.gov study NCT03229798. IPD Sharing: UNDECIDED. Countries: 1. Publications: 3.
MCB vs EUS-FNA for Preoperative Pathological Evaluation of Gastric SMT
ClinicalTrials.gov study NCT06748690. IPD Sharing: NO. Countries: 1. Publications: 3.
Dose Response Effects of Cervical Spinal Manipulative Therapy (SMT) on Pressure Sensitivity of Myofascial Trigger Points
ClinicalTrials.gov study NCT01418170. IPD Sharing: Not stated. Countries: 1. Publications: 37.
Modified Diet Trial: A Study of SMT C1100 in Paediatric Patients With DMD Who Follow a Balanced Diet
ClinicalTrials.gov study NCT02383511. IPD Sharing: Not stated. Countries: 1. Publications: 1.
Dataset for "Adding the SMT solver OpenSMT2 to the JavaSMT Framework and Evaluation using CPAchecker"
<p>Benchmark data and code examples for the thesis. See README.md files for the exact locations.</p>
Study to Evaluate the Safety and Efficacy of High Dose Intravenous Immune Globulin (IVIG) Plus Standard Medical Treatment (SMT) Versus SMT Alone in Participants in Intensive Care Unit (ICU) With Coron
ClinicalTrials.gov study NCT04480424. IPD Sharing: NO. Countries: 1. Publications: 0.
Proof of Concept Study to Assess Activity and Safety of SMT C1100 (Ezutromid) in Boys With Duchenne Muscular Dystrophy (DMD)
ClinicalTrials.gov study NCT02858362. IPD Sharing: Not stated. Countries: 2. Publications: 0.
Benchmark results for JavaSMT code-generator and parser-interpreter for SMT-LIB2
<p>The new integration of a code-generator and parser-interpreter for SMT-LIB2 into JavaSMT [1] was benchmark tested with CPAchecker [2], the Benchexec framework [3] using the included run definition '<a href="../api/records/10307339/draft/files/princess_run.xml/content">princess_run.xml</a>' and SV-Benchmarks [4]. The results are available in '<a href="../api/records/10307339/draft/files/results.2023-11-28_17-09-38.table.csv/content">results.2023-11-28_17-09-38.table.csv</a>' and '<a href="../api/records/10307339/draft/files/results.2023-11-28_17-09-38.table.csv/content">results.2023-11-28_17-09-38.table.csv</a>'. The log files for each individual task can be found in <a href="../api/records/10307339/draft/files/results.zip/content">results.zip. </a></p> <p>[1] github.com/sosy-lab/java-smt/pull/343</p> <p>[2] svn.sosy-lab.org/software/cpachecker/branches/javasmt-smtlib2-generator-parser/</p> <p>[3] github.com/sosy-lab/benchexec/releases/tag/3.20</p> <p>[4] gitlab.com/sosy-lab/benchmarking/sv-benchmarks, commit 509aa682</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.