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.
221
datasets available to search
ShareScore release 0.9.0
Dataset results
221 results for “formalization”
Experimenting with Formal Verification and Model-based Development in Railways: the case of UMC and Sparx Enterprise Architect - Complementary Data
<p>This repository contains the UMC and SPARX EA data used in the paper:</p> <p>Experimenting with Formal Verification and Model-based Development in Railways: the case of UMC and Sparx Enterprise Architect</p> <p>by Davide Basile, Franco Mazzanti and Alessio Ferrari.</p>
Dataset for : A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification
<p>We present a novel solution combining Large Language Model (LLM) capabilities with Formal Verification strategies to falsify and automatically repair software vulnerabilities. Initially, we employ Bounded Model Checking (BMC) to locate the software vulnerability and derive a counterexample. Relying on mathematical proofs, counterexamples provide evidence that the system behaves incorrectly or contains a vulnerability, thereby preventing the generation of false positive alerts. The counterexample that has been detected, along with the source code, are provided to the LLM engine. Our approach involves establishing a specialized prompt language for conducting code debugging and generation to understand the vulnerability's root cause and repair the code. Finally, we use BMC to verify the corrected version of the code generated by the LLM. As a proof of concept, we create \esbmcai based on the Efficient SMT-based Context-Bounded Model Checker (ESBMC) and a pre-trained Transformer model, specifically gpt-3.5-turbo, to detect and fix errors in C programs. We generated a dataset comprising $1{,}000$ C code samples, each consisting of $20$ to $50$ lines of C code. Experimental results show that our proposed method achieved an impressive success rate of up to $80$\% in repairing vulnerable code, encompassing buffer overflow, arithmetic overflow, and pointer dereference failures. To our knowledge, \esbmcai represents the first proposal for a pioneering initiative to integrate a Large Language Model (LLM) with software model checking. We advocate that this automated approach has the potential to incorporate into the software development lifecycle's continuous integration and deployment (CI/CD) process. </p> <p> </p> <p>The uploaded dataset contains 1000 codes, each comprising 20 to 50 lines of C code generated with gpt-3.5-turbo. The material also consists of a version of ESBMC statically compiled with all dependencies, a classifier script, and the output file.</p> <p> </p> <p> </p>
MLFMF: Data Sets for Machine Learning for Mathematical Formalization
<h3>MLFMF</h3><p><strong>MLFMF (Machine Learning for Mathematical Formalization) </strong>is a collection of data sets for benchmarking recommendation systems used to support formalization of mathematics with proof assistants. These systems help humans identify which previous entries (theorems, constructions, datatypes, and postulates) are relevant in proving a new theorem or carrying out a new construction. </p><p>The MLFMF data sets provide solid benchmarking support for further investigation of the numerous machine learning approaches to formalized mathematics. With more than 250,000 entries in total, this is currently the largest collection of formalized mathematical knowledge in machine learnable format. </p><p>In addition to benchmarking the recommendation systems, the data sets can also be used for benchmarking <strong>node classification</strong> and <strong>link prediction</strong> algorithms. </p><h3>The four data sets</h3><p>Each data set is derived from a library of formalized mathematics written in proof assistants <a href="https://agda.readthedocs.io/en/v2.6.4/"><i>Agda</i></a> or <a href="https://lean-lang.org/"><i>Lean</i></a>. The collection includes </p><ol><li>the largest Lean 4 library <a href="https://github.com/leanprover-community/mathlib4"><strong>Mathlib</strong></a>,</li><li>the three largest Agda libraries:<ul><li>the <a href="https://github.com/agda/agda-stdlib"><strong>standard library</strong></a></li><li>the library of univalent mathematics <a href="https://github.com/UniMath/agda-unimath"><strong>Agda-unimath</strong></a>, and</li><li>the <a href="https://github.com/martinescardo/TypeTopology"><strong>TypeTopology</strong></a> library.</li></ul></li></ol><p>Each data set represents the corresponding library in two ways: as a heterogeneous network, and as a list of syntax trees of all the entries in the library. The network contains the (modular) structure of the library and the references between entries, while the syntax trees give complete and easily parsed information about each entry.</p><p>The Lean library data set was obtained by converting <strong>.olean</strong> files into s-expressions (see the <a href="https://github.com/andrejbauer/lean2sexp"><strong>lean2sexp</strong></a> tool).</p><p>The Agda data sets were obtained with an <a href="https://github.com/andrejbauer/agda/tree/master-sexp">s-expression extension</a> of the official Agda repository (use either master-sexp or release-2.6.3-sexp branch).</p><p>For more details, see our <a href="https://arxiv.org/abs/2310.16005"><strong>arXiv copy</strong></a><strong> </strong>of the paper.</p><h3>Directory structure</h3><p>First, the <strong>mlfmf.zip</strong> archive needs to be unzipped. It contains a separate directory for every library (for example, the standard library of Agda can be found in the stdlib directory) and some auxiliary files. Every library directory contains</p><ul><li>the <strong>network file</strong> from which the heterogeneous network can be loaded,</li><li>a zip of the <strong>entries directory</strong> that contains (many) files with abstract syntax trees. Each of those files describes a single entry of the library.</li></ul><p>In addition to the auxiliary files which are used for loading the data (and described below), the zipped sources of lean2sexp and Agda s-expression extension are present.</p><h4>Loading the data</h4><p>In addition to the data files, there is also a simple python script <strong>main.py</strong> for loading the data. To run it, you will have to install the packages listed in the file <strong>requirements.txt</strong>: <strong>tqdm</strong> and <strong>networkx</strong>. The easiest way to do so is calling <i><strong>pip install -r requirements.txt</strong></i>.</p><p>When running <strong>main.py </strong>for the first time, the script will unzip the entry files into the directory named <strong>entries</strong>. After that, the script loads the syntax trees of the entries (see the <strong>Entry</strong> class) and the network (as <i>networkx.MultiDiGraph</i> object).</p><p><i>Note. The entry files have extension <strong>.dag </strong>(directed acyclic graph), since Lean uses node sharing, which breaks the tree structure (a shared node has more than one parent node).</i></p><h3>More information</h3><p>For more information about the <strong>data collection process</strong>, <strong>detailed data (and data format) description</strong>, and <strong>baseline experiments</strong> that were already performed with these data, see our <a href="https://arxiv.org/abs/2310.16005"><strong>arXiv copy</strong></a><strong> of the paper</strong>.</p><p>For the code that was used to perform the experiments and data format description, visit our github repository <a href="https://github.com/ul-fmf/mlfmf-data"><strong>https://github.com/ul-fmf/mlfmf-data.</strong></a></p><h3>Funding</h3><p>Since not all the funders are available in the Zenodo's database, we list them here:</p><ol><li>This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0024.</li><li>The authors also acknowledge the financial support of the Slovenian Research Agency via the research core funding No. P2-0103 and No. P1-0294.</li></ol><p> </p>
Survey data on financial literacy, financial inclusion, informal financial business practices, and intentions towards formalization of female small vendors in Lima, Peru
<p><span>This dataset encapsulates a comprehensive survey aimed at understanding informal business practices and financial literacy among small business vendors in Peru. The dataset comprises three key components: the survey questionnaire, raw survey data, and a detailed codebook. Researchers interested in the dynamics of financial practices in emerging markets may find this dataset particularly valuable, as it allows for the exploration of factors influencing financial decisions in small enterprises, with potential modifications suggested for adapting the survey to different national or cultural contexts. This dataset not only contributes to empirical research in financial behavior but also supports gender-specific studies by allowing the variable 'sex' to be adapted to 'gender' with multiple response options. </span></p> <p><span>The data and supplementary material is divided in tree files:</span></p> <p><span>The survey, presented in "Survey IFE.docx," includes questions across various domains such as informal business practices, financial literacy, financial inclusion, intentions towards financial formalization, and the formality of business ventures, along with demographic variables like age, sex, business age, and number of employees. </span></p> <p><span>The raw data, stored in "Dataset.csv," records responses from 118 participants, mapped against 31 indicators. </span></p> <p><span>The "Codebook.doc" provides exhaustive details about the survey variables, coding of responses, and the methodology employed, facilitating the replication of the study and application of the dataset in varied research contexts.</span></p>
Improving Formal Verification with Portfolio-based Runtime Techniques: Dataset
<p>Evaluation Dataset of the Scientific Students’ Association Report titled Improving Formal Verification with Portfolio-based Runtime Techniques</p>
The 2020 Comparison of Tools for the Analysis of Quantitative Formal Models: Results and Reproduction
<p>This archive contains detailed results from QComp 2020 as well as the necessary scripts and data to reproduce them.</p> <p>Visit http://qcomp.org for more information for QComp.</p> <p>Overview of Contents</p> <p>- `qcomp.org/` contains the state of our website from the timepoint of the competition. This includes:<br> - All benchmark files, browsable at `qcomp.org/benchmarks/index.html`<br> - Detailed competition results in a human-readable format, browsable at `https://qcomp.org/competition/2020/`<br> - `logs/` contains the raw logfiles and data gathered by our scripts<br> - `scripts/` contains scripts to replicate the whole competition<br> - `toolpackages/` contains a package for each participating tool which includes<br> - Instructions for obtaining and installing the tool<br> - a file `invocations.json` listing the commandlines used in QComp 2020<br> - a file `tool.py` providing functionalities to obtain the result from the tool output.</p>
Systematic Evaluation and Usability Analysis of Formal Tools for Railway System Design - Technical Annexes
<p>This package includes additional data for the paper ``Systematic Evaluation and Usability Analysis of Formal Methods Tools for Railway Signalig System Design'', by Alessio Ferrari, Franco Mazzanti, Davide Basile, and Maurice ter Beek, CNR-ISTI, Italy, accepted for publication in the IEEE Transactions on Software Engineering, DOI: 10.1109/TSE.2021.3124677</p> <p>The paper concerns the systematic evaluation and usability analysis of 14 formal tools for system design, namely CADP (2020-g), FDR4(4.2.7), NuSMV(1.1.1), ProB(1.9.3), Atelier B (4.5.1), Simulink (R2020a), SPIN (6.4.9), UMC (4.8), UPPAAL (4.1.4), mCLR2 (202006.0), SAL (3.3), TLA+ (2) and CPN Tools (4.0). The current package includes the following content:</p> <ol> <li>Tool Evaluation Template and .pdf: a document including the reference evaluation template, and the evaluation sheet of each tool. </li> <li>Tool Evaluation Table.xlsx: a table summarizing the results of the evaluation.</li> <li>System Usability Test - SUS Results.xlsx: an excel file with multiple sheets with all the raw results of the usability test for the tools.</li> </ol>
SMTLIB2.6 translation of proof obligations from the B formal method
<p>These files have been produced from the <a href="https://doi.org/10.5281/zenodo.7050797">POG files</a> using the program ppTransSmt, distributed with Atelier B.</p> <p>The source code of this version of ppTransSmt correspond to git commit `abb8ad04003803ea3683d8069363681e92308ebf` (in the private repository<br> of Atelier B).<br> </p>
Proof obligations from the B formal method
<p>Proof obligations generated with Atelier B, an IDE for the B method and Event-B.</p> <p>The files are in the POG format.</p>
Supplementary Material for "Formal methods in dependable systems engineering: a survey of professionals from Europe and North America"
<p>This report contains supplemental material for <a href="https://link.springer.com/article/10.1007%2Fs10664-020-09836-5">this paper</a>, including a detailed analysis of responses to certain questions, further visualizations of the collected data, details on our analysis of related work, and a copy of the whole questionnaire. This material was shared for the period of peer review and has been significantly updated, extended, and included in <a href="https://link.springer.com/article/10.1007%2Fs10664-020-09836-5">this journal publication</a>.</p>
NMR data of all compounds appearing in the study "Visible Light-Mediated Formal Alkylation and [4+1]-Cycloaddition Strategies of Silyl Enol Ethers with Aryldiazoacetates"
<p>FID files of NMR data (<em>e.g.</em> 1H, 13C{1H}, 19F{1H}, COSY, HSQC, DEPT135 and HMBC) associated with all compounds synthesized during the study entitled "Visible Light-Mediated Reactions of Silyl Enol Ethers with Aryldiazoacetates: Formal Alkylation and [4+1]-Cycloaddition Strategies" (a research project in organic synthesis)</p>
Formal Methods in Railways: a Systematic Mapping Study - List of Primary Studies and Data Extraction
<p>This Excel file includes the list of papers analyzed in the systematic mapping study titled "Formal Methods in Railways: a Systematic Mapping Study". The study has been submitted for publication, and its preprint is also included in this repository. </p>
Data, code and software to reproduce the article entitled "Modeling soil-plant functioning of intercrops using comprehensive and generic formalisms implemented in the STICS model"
<p>This is the data, code and software to reproduce the article entitled " Modeling soil-plant functioning of intercrops using comprehensive and generic formalisms implemented in the STICS model". Here is a summary of the paper:</p> <p>The growing demand for sustainable agriculture is raising interest in intercropping for its multiple potential benefits to avoid or limit the use of chemical inputs or increase the production per surface unit. Predicting the existence and magnitude of those benefits remains a challenge given the numerous interactions between interspecific plant-plant relationships, their environment and the agricultural practices. Soil-crop models are critical in understanding these interactions in dynamics during the whole growing season, but few models are capable of accurately simulating intercropping systems.</p> <p>In this study, we propose a set of simple and generic formalisms for simulating key interactions in intercropping systems that can be readily included into existing dynamic crop models. This requires simulating important processes such as development, light interception, plant growth, N and water balance, and yield formation in response to management practices, soil conditions, and climate. These formalisms were integrated into the STICS soil-crop model and evaluated using observed data of intercropping systems of cereal and legumes mixtures, including Faba bean-Wheat, Pea-Barley, Sunflower-Soybean, and Wheat-Pea mixtures. We demonstrate that the proposed formalisms provide a comprehensive simulation of soil-plant interactions in various types of bispecific intercrops. The model was found consistent and generic under a range of spring and winter intercrops (nRMSE = 25% for maximum leaf area index, 23% for shoot biomass at harvest, and 18% for yield).</p> <p>This is the first time a complete set of formalisms has been developed and published for simulating intercropping systems and integrated into a soil-crop model. With its emphasis on being generic, sufficiently accurate, simple, and easy to parameterize, STICS is well-suited to help researchers designing <em>in silico</em> the agroecological transition by virtually pre-screening sustainable, manageable intercrop systems adapted to local conditions.</p> <p> </p> <p> </p> <p> </p>
Dataset for "A general purpose potential for glassy and crystalline phases of Cu-Zr alloys based on the ACE formalism"
<p>This dataset was used to fit a general purpose machine learning interatomic potential for the Cu-Zr system. It supports the paper "A general purpose potential for glassy and crystalline phases of Cu-Zr alloys based on the ACE formalism".</p>
FM-Tools Release 2.2: Data Set of Metadata about Tools for Formal Methods (SV-COMP 2025, Test-Comp 2025)
<h1>Collection of Information about Formal-Methods Tools</h1> <h2>Motivation</h2> <p>There are many tools available that implement formal-methods approaches. This repository collects meta data about the tools, such that it becomes easier to reuse, integrate, and cooperate with formal-methods tools.</p> <p>A <a href="https://www.sosy-lab.org/research/pub/2024-Podelski65.Find_Use_and_Conserve_Tools_for_Formal_Methods.pdf">description</a> of the structure of this repository can be found in an article.</p> <p>A <a href="https://fm-tools.sosy-lab.org/">formatted listing</a> of some of the data in this repository can be found on a generated web site.</p> <p>A <a href="https://fm-tools.sosy-lab.org/schema.html">schema definition</a> of the data files in this repository can be found on a generated web site.</p>
Formalizing Objectives and Criteria for Urban Agriculture Sustainability with a Participatory Approach
<p>The last few years have seen an exponential development of urban agriculture projects within global North countries, especially professional intra-urban farms which are professional forms of agriculture located within densely settled areas of city. Such projects aim to cope with the challenge of sustainable urban development and today the sustainability of the projects is questioned. To date, no set of criteria has been designed to specifically assess the environmental, social and economic sustainability of these farms at the farm scale. Our study aims to identify sustainability objectives and criteria applicable to professional intra-urban farms. It relies on a participatory approach involving various stakeholders of the French urban agriculture sector comprising an initial focus group, online surveys and interviews. We obtained a set of six objectives related to environmental impacts, link to the city, economic and ethical meaning, food and environmental education, consumer/producer connection and socio-territorial services. In addition, 21 criteria split between agro-environmental, socio-territorial and economic dimensions were identified to reach these objectives. Overall, agro-environmental and socio-territorial criteria were assessed as more important than economic criteria, whereas food production was not mentioned. Differences were identified between urban farmers and decision makers, highlighting that decision makers were more focused on projects' external sustainability. They also pay attention to the urban farmer agricultural background, suggesting that they rely on urban farmers to ensure the internal sustainability of the farm. Based on our results, indicators could be designed to measure the sustainability criteria identified, and to allow the sustainability assessment of intra-urban farms.</p>
Efficient Techniques for Formal Verification of C Programs: SV-COMP 2022 dataset
<p>This dataset contains the data on the last set of pre-run benchmarks of the tool Theta on SV-COMP 2022. The benchmarks were executed by the SV-COMP 2022 organizers, but a short evaluation of these are added in the Bachelor's Thesis with the title Efficient Techniques for Formal Verification of C programs.</p> <p>This dataset archives these benchmark results so they are always available to the reader's of this thesis.</p> <p>The html and csv files are generated with the table-generator utility of Benchexec from the .xml.bz2 files. One contains the results of the Concurrency Safety category only, while the other contains all categories.</p>
Data for 'Formalizing Artisanal and Small-scale Gold Mining: a Grand Challenge of the Minamata Convention'
<p>Signatories to the Minamata Convention on Mercury with ‘more than insignificant’ artisanal and small-scale gold mining (ASGM) sectors are required to develop and implement National Action Plans (NAPs) to reform their ASGM sectors in line with Annexe C of the Convention. We compiled the budgets of available NAPs for reducing mercury emissions from ASGM sectors. As of 2021-12-31, these were available for 16 countries from: www.mercuryconvention.org/en/parties/national-action-plans. We used these data to estimate the approximate costs of expanding such approaches globally.</p>
Supporting material for "Impact of gender on the formation and outcome of formal mentoring relationships in the life sciences"
<p>This repository contains data and analysis code associated with the manuscript: L.P. Schwartz, J. Liénard, S. V. David. (2022) "Impact of gender on formation and outcome of formal mentoring relationships in the life sciences." Figures and tables in the manuscript can be produced by running the make_figures.ipynb notebook. Figures have been marked with headings indicating their position in the manuscript (Figure 1, Figure S1, etc.). In addition, the notebook contains code to reproduce regression analyses that are cited in the text but not directly associated with a figure.</p> <p>Data on mentoring relationships derives from Academic Family Tree (AFT, www.academictree.org) and public data sources on funding, publications, and awards. Inclusion criteria, public data sources, and procedures for linking across sources are described in the manuscript. Personal identifiers for researchers have been anonymized, but remain consistent across all data in the repository. In other words, the personal identifier "1" refers to the same person in all dataframes in the repository. But, that person is *not* the same researcher identified as "1" on the public AFT website.</p> <p><strong>Installation</strong></p> <p>Requires Python 3.x. and Pandas. To load required libraries using Anaconda, run:</p> <p>`conda create --name aft -c conda-forge pandas numpy scipy ipython jupyterlab scipy scikit-learn pandas matplotlib numpy statsmodels seaborn pytables`</p> <p><strong>Dataframes</strong></p> <p>Data is stored as a series of Pandas dataframes within HDF5 or CSV files:</p> <p>* cng_tc: The primary dataset used in the analysis. The name is an acronym for "connections" (i.e. training relationships, "cn"), "gender" ("g"), and "trainee count" ("tc"). Each row contains data on the mentor and trainee in one training relationship. See manuscript for inclusion criteria.</p> <p>* mentors: Data on mentors. Each row contains data on one mentor. See manunscript for inclusion criteria.</p> <p>* mentors_grants, mentors_hindex, mentors_locs_ranked: Subset of mentors with data available for funding (mentors_grants), citation (mentors_hindex), and institution rank (mentors_locs_ranked).</p> <p>* mentors_nobel, mentors_hhmi, mentors_nas: Subsets of mentors that received a Nobel (mentors_nobel), Howard Hughes Medical Institute grants (mentors_hhmi), or membership in the National Academy of Sciences (mentors_nas). See manuscript for details of data sources and linking procedures.</p> <p>* cn, cng, first_names, gn, gn_all, locs: Partial data (connections only, inferred gender only, connections and gender only, location only, first names and inferred gender only) for more inclusive sets of researchers in AFT. They are generally not used used for analysis, but have been included here to calculate statistics on the total amount of data included and to screen for data from U.S. locations.</p> <p>* nsf_gender_phds, nsf_gender_pds: National Science Foundation survey data on gender and fraction PhDs conferred per year (nsf_gender_phds) or fraction postdocs employed per year (nsf_gender_pds). See manuscript for details of data source.</p> <p>* photo: Data for validation of gender inference method.</p> <p><strong>Dataframe columns</strong></p> <p>* amount: Mentor's total funding<br> * amount_adj: Mentor's total funding (adjusted to 2020 dollars)<br> * broad_field: Mentor's general research area (e.g., life sciences, engineering, based on National Science Foundation classifications)<br> * continue: Whether trainee went on to become a mentor (i.e., has trainees listed in AFT)<br> * country: Country in which mentor's current institution is located<br> * firstname: First name of researcher (table of first names is not aligned with tables containing anonymized personal identifiers)<br> * first_grant_year: Year of mentor's first grant<br> * funding_rate: Mentor's annual funding rate (since first grant)<br> * funding_rate_adj: Mentor's annual funding rate (since first grant) adjusted to 2020 dollars<br> * hhmi: Whether mentor was granted HHMI funding<br> * hindex: Mentor's hindex<br> * location: Name of mentor's current institution<br> * locid: Identifier for mentor's institution<br> * locid_rank: Postion of mentor's institution in 2015 Quacquarelli-Symonds rankings (lower numbers are better)<br> * locid_rank_rev: Reversed version of "locid_rank" (i.e., higher numbers are better)<br> * majorarea: Mentor's specific research area (e.g, neuroscience)<br> * male_mentor, male trainee: Whether the probability that a researcher's first name is used by a person identifying as a man meets threshold (see manuscript for details on gender inference using first names)<br> * match_score: Score for string match between institution or name of awardee and researcher<br> * mentor_career_start: The date at which the mentor's academic career began<br> * mentor_continue_rate: Fraction of mentor's trainees that become mentors<br> * mentor_continue_rate_ft: Fraction of mentor's woman trainees that become mentors<br> * mentor_continue_rate_mt: Fraction of mentor's man trainees that become mentors<br> * mentor_t_p_male0: Fraction of mentor's trainees that are men<br> * mentor_t_p_male0_gs: Fraction of mentor's trainees that are men (graduate students only)<br> * mentor_t_p_male0_pd: Fraction of mentor's trainees that are men (postdocs only)<br> * mentor_tcount0: Mentor's total number of trainees<br> * nas: Whether mentor is a member of the National Academy of Sciences<br> * nobel: Whether mentor is a Nobel laureate<br> * p_male_mentor, p_male_trainee: Probability that a researcher's first name is used by a person identifying as a man<br> * pid: Anonymized identifier of researcher<br> * pid_mentor: Anonymized identifier of mentor in training relationship<br> * pid_trainee: Anonymized identifier of trainee in training relationship<br> * pq: "1" if data on training relationship is drawn from ProQuest database and has not been manually edited a human AFT user<br> * relation: Type of training relationship (1: graduate student, 2: postdoc)<br> * scorer1, scorer2, scorer3: Results of photo validation of gender inference for each scorer<br> * start: Training start year<br> * stop: Training end year<br> * trainee_tcount: Total people that the trainee has trained<br> * triad: Whether trainee has participated in both a graduate-level and postdoctoral training relationship</p> <p>The cn dataframe follows slightly different naming conventions, but is not generally used in the analysis (pid1 = pid_trainee, pid2 = pid_mentor, startdate = start, stopdate = stop).</p>
Fig. 1. Type RNHL 1809 in Extinction of Japan's first formally described earthworm (Horst, 1883) (Annelida, Oligochaeta, Megadrilacea, Megascolecidae).
Fig. 1. Type RNHL 1809 of Amynthas japonicus in Leiden (courtesy of J. Bleeker Sept., 2016). This is the only known specimen and image of this Japanese species (cf. M. sieboldi – http://www. geocities.jp/at_mocha/mimizu/sieboldi-3.html).
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.