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.
42
datasets available to search
ShareScore release 0.9.0
Dataset results
42 results for “model checking”
CNF Encoded Isomorphic and Optimized Miters from Hardware Model Checking Competition 2012 Models
<p>These miter benchmarks are used in a paper on congruence closure in 2024.</p> <p>The miter AIGs in the [`aig`](aig) directory are the same as those used to<br>generate CNFs of miter benchmarks submitted to the SAT Challenge in 2012.<br>Some of them have regularly been used in the SAT Competitions since then.</p> <p>The AIGs are separated into two sets:</p> <p>- [`aig/iso`](aig/iso) miters of isomorphic circuits<br>- [`aig/opt`](aig/opt) miters of optimized versus original circuit</p> <p>The first set checks equivalence of one circuit with itself in the<br>[`aig/iso`](aig/iso) (isomorphic) sub-directory and second set contains<br>equivalence checking problems (aka miters) comparing the original circuit<br>with an optimized version in the [`aig/opt`](aig/opt) (optimized)<br>sub-directory. The optimized versions of the circuits were obtained in 2012<br>by the `dc2` script for [ABC](https://people.eecs.berkeley.edu/~alanmi/abc).<br>We did not re-run ABC with a newer version in order to make sure we have as<br>base-line in our experiments the same CNFs, as they are well-known, i.e., <br>they have been used in the SAT competitions for several years.</p> <p>Note that the original AIGER models have state elements (called "latches"<br>in AIGER terminology), but both the optimization with ABC as well as our<br>equivalence checking is purely combinational, by treating latches as<br>additional pseudo inputs, and next-state functions as output-functions. The<br>miters were accordingly generated (by the 2011 version) of `aigmiter` using<br>the `-c` option. For the same reason as for ABC explained above, we did not<br>rerun `aigmiter` either.</p> <p>We then encoded the two sets of AIGs into CNF in two different ways.<br>The first encoding just uses a simple Tseitin encoding, without<br>Plaisted-Greenbaum optimization, i.e., using the `--no-pg` option, as in 2012.<br>Even though we use a new version of `aigtocnf` in `src/aiger/aigtocnf.c` we<br>made sure that identical CNFs are generated for this first encoding variant<br>by checking that the MD5 sum of the (actually compressed) CNF files match.<br>This required to disable a newly introduced cone-of-influence (COI)<br>optimization with `--no-coi` which skips unreachable gates even when the<br>Plaisted-Greenbaum optimization is disabled.</p> <p>The second variant of the encoding detects XOR and ITE gates by pattern<br>matching and produces more concise CNFs by skipping internal AND gates<br>of detected XOR and ITE gates producing a direct encoding instead.</p> <p>This gives the following sets of CNFs;</p> <p>- [`cnf/ands/iso`](cnf/ands/iso) isomorphic circuits with ANDs only<br>- [`cnf/ands/opt`](cnf/ands/opt) optimized versus original with ANDs only<br>- [`cnf/xits/iso`](cnf/xits/isor) isomorphic circuits with ANDs, XORs, ITEs<br>- [`cnf/xits/opt`](cnf/xits/opt) optimized versus original with ANDs, XORs, ITEs</p> <p>All the CNFs in these directories have the same original file name of the<br>AIGER model to simplify run-time comparison. In `cnf/all` we further<br>provide links with qualified names to distinguish them.</p>
CNF Encoded Isomorphic and Optimized Miters from Hardware Model Checking Competition 2020 Models
<p>From the Hardware Model Checking Competition 2020 we have collected 324<br>sequential model checking problems and for each generated an isomorphic and<br>an optimized miter. The isomorphic miters just compares two identical<br>copies while for the optimized miter one copy went through optimization<br>with ABC using the `dc2` command.</p> <p>The CNFs are generated with a new version of `aigtocnf` which detects<br>XOR and ITE gates in the AIGER circuit and if detected uses a more compact<br>encoding (4 clauses clauses instead of 9) for each detected gate.</p>
Artifact for 'Unfolding State Variables Improves Model Checking'
<p>This is a reproduction package for the experiments that were performed as part of the work 'Unfolding State Variables Improves Model Checking'.</p>
Data for paper "Parametric Timed Model Checking for Guaranteeing Timed Opacity"
<p>Our zip contains all necessary scripts, models, binaries and instructions to reproduce the experiments of our paper<br> <em>Parametric Timed Model Checking for Guaranteeing Timed Opacity</em> published in the proceedings of ATVA 2019.</p> <p>It allows interested readers to reproduce exactly the content of <strong>Table 1</strong> and <strong>Table 2</strong> of our paper.<br> In addition, all result files are generated, containing the synthesized constraints, and the execution times of IMITATOR.</p>
Probabilistic Model Checking for Temporal Logics in Weighted Structures - Experiments
<p>Supplementary material for the thesis</p> <p>Probabilistic Model Checking for Temporal Logics in Weighted Structures</p> <ul> <li>data set for the experiments</li> <li>results of the experiments</li> <li>evaluation scripts</li> </ul>
Runtime Monitoring of Refinement Progress in CEGAR-based Model Checking: Dataset
<p>Dataset used in the evaluation of Part II of the MSc thesis titled "Extending the Capabilities of the CEGAR Model Checking Algorithm"</p>
PLCspecif permissive equivalence checking example model
<p>Example models for the permissive equivalence checking relations of PLCspecif.</p>
Figure 6 from: Cecchetto M, Alvaro MC, Ghiglione C, Guzzi A, Mazzoli C, Piazza P, Schiaparelli S (2017) Distributional records of Antarctic and sub-Antarctic Ophiuroidea from samples curated at the Italian National Antarctic Museum (MNA): check-list update of the group in the Terra Nova Bay area (Ross Sea) and launch of the MNA 3D model 'virtual gallery'. ZooKeys 705: 61-79. https://doi.org/10.3897/zookeys.705.13712
Figure 6 - Number of individuals by preservation method stored at MNA. Dried specimens percentage in orange (~80%), ethanol in blue (~15%), and frozen in green (~5%)
Figure 7 from: Cecchetto M, Alvaro MC, Ghiglione C, Guzzi A, Mazzoli C, Piazza P, Schiaparelli S (2017) Distributional records of Antarctic and sub-Antarctic Ophiuroidea from samples curated at the Italian National Antarctic Museum (MNA): check-list update of the group in the Terra Nova Bay area (Ross Sea) and launch of the MNA 3D model 'virtual gallery'. ZooKeys 705: 61-79. https://doi.org/10.3897/zookeys.705.13712
Figure 7 - Video of the 3D model of O. echinulata (MNA 2644); Catalogue number, latitude (DD), longitude (DD), depth and event date as described in the section "Dataset description", GenBank Accession number, Barcode Index Number from the Bold system and the complete COI sequence in FASTA format. Video available at: https://youtu.be/Sq6au-_CHy0
Figure 2 from: Cecchetto M, Alvaro MC, Ghiglione C, Guzzi A, Mazzoli C, Piazza P, Schiaparelli S (2017) Distributional records of Antarctic and sub-Antarctic Ophiuroidea from samples curated at the Italian National Antarctic Museum (MNA): check-list update of the group in the Terra Nova Bay area (Ross Sea) and launch of the MNA 3D model 'virtual gallery'. ZooKeys 705: 61-79. https://doi.org/10.3897/zookeys.705.13712
Figure 2 - Overview map depicting the wideness of the area containing the sampling stations of the dataset. Areas in red are shown in detail in figures 3, 4 and 5.
Figure 5 from: Cecchetto M, Alvaro MC, Ghiglione C, Guzzi A, Mazzoli C, Piazza P, Schiaparelli S (2017) Distributional records of Antarctic and sub-Antarctic Ophiuroidea from samples curated at the Italian National Antarctic Museum (MNA): check-list update of the group in the Terra Nova Bay area (Ross Sea) and launch of the MNA 3D model 'virtual gallery'. ZooKeys 705: 61-79. https://doi.org/10.3897/zookeys.705.13712
Figure 5 - Map with the sampling sites in the Falkland Islands (Islas Malvinas) and Bransfield Strait
Figure 1 from: Cecchetto M, Alvaro MC, Ghiglione C, Guzzi A, Mazzoli C, Piazza P, Schiaparelli S (2017) Distributional records of Antarctic and sub-Antarctic Ophiuroidea from samples curated at the Italian National Antarctic Museum (MNA): check-list update of the group in the Terra Nova Bay area (Ross Sea) and launch of the MNA 3D model 'virtual gallery'. ZooKeys 705: 61-79. https://doi.org/10.3897/zookeys.705.13712
Figure 1 - Flowchart depicting major steps in dataset development and publishing, from sample collection to the production of a virtual collection of the museum's 3D vouchers.
Figure 4 from: Cecchetto M, Alvaro MC, Ghiglione C, Guzzi A, Mazzoli C, Piazza P, Schiaparelli S (2017) Distributional records of Antarctic and sub-Antarctic Ophiuroidea from samples curated at the Italian National Antarctic Museum (MNA): check-list update of the group in the Terra Nova Bay area (Ross Sea) and launch of the MNA 3D model 'virtual gallery'. ZooKeys 705: 61-79. https://doi.org/10.3897/zookeys.705.13712
Figure 4 - Highlight of the sampling sites in Terra Nova Bay (a sampling locations from 1988 to 2004 b sampling locations from 2009 to 2014), Cape Hallett (c) and Cape Adare (d) areas.
Figure 8 from: Cecchetto M, Alvaro MC, Ghiglione C, Guzzi A, Mazzoli C, Piazza P, Schiaparelli S (2017) Distributional records of Antarctic and sub-Antarctic Ophiuroidea from samples curated at the Italian National Antarctic Museum (MNA): check-list update of the group in the Terra Nova Bay area (Ross Sea) and launch of the MNA 3D model 'virtual gallery'. ZooKeys 705: 61-79. https://doi.org/10.3897/zookeys.705.13712
Figure 8 - Video of the 3D model of O. antarctica (MNA 7784); Catalogue number, latitude (DD), longitude (DD), depth and event date as described in the section "Dataset description"; GenBank Accession number, the Barcode Index Number from the Bold system and the complete COI sequence in FASTA format. Video available at: https://youtu.be/Z72GryamWZY
Figure 9 from: Cecchetto M, Alvaro MC, Ghiglione C, Guzzi A, Mazzoli C, Piazza P, Schiaparelli S (2017) Distributional records of Antarctic and sub-Antarctic Ophiuroidea from samples curated at the Italian National Antarctic Museum (MNA): check-list update of the group in the Terra Nova Bay area (Ross Sea) and launch of the MNA 3D model 'virtual gallery'. ZooKeys 705: 61-79. https://doi.org/10.3897/zookeys.705.13712
Figure 9 - a The A. agassizii (MNA 7368) specimen used for photogrammetry documented immediately after collecting b screenshot of the 3D model based on photogrammetry at the mesh reconstruction stage (the marker showed as model background is available as supplementary material in Porter et al. 2016); Catalogue number, latitude (DD), longitude (DD), depth and event date as described in the section "Dataset description"; GenBank Accession number, the Barcode Index Number from the Bold system and the complete COI sequence in FASTA format.
What is the Best Algorithm for MDP Model Checking? Replication Package
<p>This artefact allows to review and replicate the experiments from the paper <strong>What is the Best Algorithm for MDP Model Checking?</strong>.<br> The package contains all original logfiles and the scripts that extract the relevant data from those logs to generate the plots as in the paper.<br> Furthermore, the artefact contains the exercised version of the model checking tool `Storm` with its dependencies and convenient installation scripts as well as all benchmark instances.<br> The user can thus replicate all experiments from the paper.<br> An appropriate subset of the experiments is given to allow a review in a timely manner. In addition, single experiments can be handpicked for replication.</p> <p><em>This is a mild adaptation of the <a href="https://doi.org/10.5281/zenodo.7509473">artefact</a> for the paper "A Practitioner's Guide to MDP Model Checking Algorithms by Hartmanns et al. (TACAS'23)".</em></p>
Data from: Posterior predictive checks of coalescent models: P2C2M, an R package
Open the record for dataset details and reuse information.
We want to check chromotin conformation changes and chromotin accesiblility. We also want to compare gene profile with and without indusilam resistant tumors in mouse genetic model
GEO Series GSE293865. Mus musculus. 6 samples. Type: Genome binding/occupancy profiling by high throughput sequencing; Expression profiling by high throughput sequencing.
Pareto Curves for Compositionally Model Checking String Diagrams of MDPs: Supplemental Material
<p>Supplemental material for the paper: Pareto Curves for Compositionally Model Checking String Diagrams of MDPs</p> <p>Submitted to TACAS 2024</p>
Figure 3 from: Cecchetto M, Alvaro MC, Ghiglione C, Guzzi A, Mazzoli C, Piazza P, Schiaparelli S (2017) Distributional records of Antarctic and sub-Antarctic Ophiuroidea from samples curated at the Italian National Antarctic Museum (MNA): check-list update of the group in the Terra Nova Bay area (Ross Sea) and launch of the MNA 3D model 'virtual gallery'. ZooKeys 705: 61-79. https://doi.org/10.3897/zookeys.705.13712
Figure 3 - Map of the Ross Sea sampling locations.
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.