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.
11
datasets available to search
ShareScore release 0.9.0
Dataset results
11 results for “formal verification”
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>
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>
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>
Towards the formal verification of data-intensive applications through metric temporal logic
p>The dataset consists of a set of model descriptions representingnbsp;span>Storm topologies. It is designed on purpose to show the approach presented in the paper quot;/span>span>Towards the formal verification of data-intensive applications through m/span>span>etric/span>span>nbsp;temporalnbsp;/span>span>logicquot; (F. Marconi, M.M. Bersani, M. Erascu and M. Rossi) which focuses on the analysisnbsp;/span>span>of bottleneck nodes of data intensive applications implemented with Storm./span>/p>
Formal Methods for NFA Equivalence: QBFs, Witness Extraction, and Encoding Verification
<p>Supplemental material to the paper.</p>
Formal Verification of Storm Topologies through D-VerT
<p>This archive includes the research data associated to the paper:<br> Formal verification of storm topologies through D-VerT. In <em>Proceedings of the Symposium on Applied Computing</em> (SAC '17). Francesco Marconi, Marcello M. Bersani, and Matteo Rossi. 2017. ACM, New York, NY, USA, 1168-1174. DOI: https://doi.org/10.1145/3019612.3019769</p> <p>Specifically it includes the UML models shown in the paper (Figures 7 and 8), the corresponding instances of the Temporal logic models automatically generated by means of the D-VerT and the output files of the experiments.</p>
Supplementary Data for Multiform: Multi-objective Evolution of Requirements Models Constrained by Formal Verification Results
<p>This data set provides supplementary material for the article "<em>Multiform: Multi-objective Evolution of Requirements Models Constrained by Formal Verification Results</em>" (to appear). It contains the following files:</p> <ul> <li><strong>experiment-input-models.zip</strong> which contains the SML input models for the EBEAS and production cell examples that were used to conduct the experiment</li> <li><strong>experiment-results.tar</strong> which contains the computed candidate SML models as well as H2 database files that contain measurements.</li> <li><strong>experiment-results.pdf</strong> which summarizes the conducted controlled experiment and results.</li> </ul> <p> </p> <p><strong>Input models</strong> (example for EBEAS)</p> <ul> <li><strong>ebeas.sml</strong> contains the actual SML input model to be evolved</li> <li><strong>ebeas.ecore</strong> contains the metamodel of the EBEAS example</li> <li><strong>ebeas.xmi</strong> contains the object system of the EBEAS example that is used for the SML realizability check</li> <li><strong>ebeas.runconfig</strong> contains the runtime configuration for ScenarioTools that binds the SML input model with the object system</li> <li><strong>ebeas.cspec</strong> contains the solution space model used by Multiform.</li> </ul> <p> </p> <p><strong>Measurements</strong> are stored in an <a href="http://h2database.com/html/main.html">H2 database</a> file. To open one of the database files for the EBEAS or production cell examples extract the appropriate zip file to a local folder, navigate to the folder in a terminal, and start H2 with the appropriate database file as follows:</p> <pre><code>java -jar h2-1.4.199.jar -url jdbc:h2:./Statistics</code></pre> <p>A web-based SQL client will open in your browser. H2 cann be obtained free of charge from their homepage.</p> <p> </p> <p>The <strong>database schema</strong> consists of three simple tables:</p> <p><strong>SMLCANDIDATESTATISTICS</strong> contains measurements for each evolved candidate SML model and consists of the following columns:<br> <strong>ALGORITHM </strong>- one of 'Random', 'NSGA2', 'tabu-75-intensify'<br> <strong>SEED </strong>- seed id for which the measurement was taken<br> <strong>ITERATION </strong>- iteration id during whch the measurement was taken<br> <strong>CANDIDATE </strong>- unique id of the evaludated candidate SML model<br> <strong>SYNTHESISTIME </strong>- synthesis time of the evaludated candidate SML model<br> <strong>O1_SCENARIOS </strong>- objective value for o1<br> <strong>O2_FRAGMENTSRATIO </strong>- objective value for o2<br> <strong>O3_ENVFRAGMENTSRATIO </strong>- objective value for o3<br> <strong>C1_REALIZABILITY </strong>- constraint value for c1<br> <strong>C2_REACHABILITY </strong>- constraint value for c1</p> <p><strong>SMLITERATIONSTATISTICS </strong>contains aggregated statistical data for each iteration and consists of the following columns:<br> <strong>ALGORITHM </strong>- one of 'Random', 'NSGA2', 'tabu-75-intensify'<br> <strong>SEED </strong>- seed id for which the data was aggregated<br> <strong>ITERATION </strong>- unique id of this aggregated iteration data<br> <strong>ITERATIONSUCCESSRATE </strong>- achieved success rate in this iteration<br> <strong>ACCUMULATEDSUCCESSRATE </strong>- achieved aggregated success reate until this iteration<br> <strong>ACCUMULATEDHYPERVOLUMEINDICATOR </strong>- achieved hypervolume until this iteration<br> <strong>NUMITERATIONPARETOEQUIVALENTCANDIDATES </strong>- number of pareto-equivalent candidate SML models in this iteration<br> <strong>NUMACCUMULATEDPARETOEQUIVALENTCANDIDATES </strong>- number of pareto-equivalent candidate SML models until this iteration<br> <strong>NUMITERATIONPARETODOMINANTCANDIDATES </strong>- number of pareto-dominant candidate SML models in this iteration<br> <strong>NUMACCUMULATEDPARETODOMINANTCANDIDATES </strong>- number of pareto-dominant candidate SML models until this iteration<br> <strong>ITERATIONSYNTHESISTIME </strong>- total synthesis time of this iteration<br> <strong>ACCUMULATEDSYNTHESISTIME </strong>- accumulated total synthesis time until this iteration</p> <p><strong>SMLSEEDSTATISTICS</strong> contains aggregated statistical data for each seed and consists of the following columns:<br> <strong>ALGORITHM </strong>- one of 'Random', 'NSGA2', 'tabu-75-intensify'<br> <strong>SEED </strong>- unique id of this aggregated seed data<br> <strong>SUCCESSRATE</strong>- achieved success rate in this seed<br> <strong>HYPERVOLUMEINDICATOR </strong>- achieved hypervolume in this seed<br> <strong>NUMPARETOEQUIVALENTCANDIDATES </strong>- number of pareto-equivalent candidate SML models in this seed<br> <strong>NUMPARETODOMINANTCANDIDATES </strong>- number of pareto-dominant candidate SML models in this seed<br> <strong>TOTALSYNTHESISTIME </strong>- total synthesis time of this seed</p> <p> </p> <p><strong>Please note</strong>: the database files contain data for algorithms 'tabu-50-intensify' and 'tabu-25-intensify' representing evaluation runs with different Tabu search configurations. However, these still need to be analyzed and <strong>experiment-results.pdf</strong> refers to '<strong>tabu-75-intensify</strong>' only.</p>
Formal verification of software architectures with SysADL Studio
<p>This short video demonstrates how to formally verify a software architecture description expressed in the <a href="https://sysadl.imd.ufrn.br">SysADL architectural language</a> using its supporting tool, SysADL Studio.</p>
Adjustable Block Analysis: Actor-based Creation of Block Summaries for Scaling Formal Verification
<p>Software quality assurance becomes more and more popular in modern software development. Fixing bugs early, reduces the cost and increases the quality of the product. Since a great portion of time is needed for debugging, assisting techniques are integrated. Many techniques use formal verification as a basis. Although formal verification is applied with great success to many software development pipelines, the scalability is still a big challenge. In this work, we introduce the concept of the distributed CPAs (configurable program analyses). The core idea is to partition the control flow automaton (CFA) of a given input program in coherent blocks with one entry and one exit node. Workers analyze every block parallely and broadcast new information to every other worker. If a block contains an error location, the block is analyzed backwards from the error location. Whenever the analysis reaches the top of the block, we ask whether other blocks can prove the error location (un)reachable. For this, we can reuse the results of previous verification runs on other blocks. Our approach is easily extensible to support any existing configurable program analysis and additionally allows an easy integration of other concepts, e.g., fault localization. This work shows and explains the implementation of a framework for distributed CPAs in CPAchecker. Furthermore, we perform a thorough evaluation of the approach, showing that our implementation is sound and matches the results of the existing predicate analysis. However, the great amount of transferred data between workers slows down the verification process causing many out-of-memory errors and timeouts. Nonetheless, the evaluation reveals the current bottle-necks and points us to potentially useful and effective improvements.</p> <p>Thesis: https://www.sosy-lab.org/research/msc/2022.Kettl.Adjustable_Block_Analysis.pdf</p>
Formal Specification and Verification of a Coordination Protocol for an Automated Air Traffic Control System
We detail all of the facets of adapting classical model checking to a real aerospace system, in- cluding deriving the formal model and a set of specifications from natural language descriptions. To ensure the model checking results are meaningful, we have to ensure that both the model and specifications correctly reflect the intentions of the designers, thus we employ model validation and property debugging techniques. We demonstrate the utility of enhancing LTL satisfiability checking by taking the fairness constraints of the system model into consideration. We argue that specification debugging in real applications deserves more attention in future research efforts, and the utility of a system formalization, model and specification debugging, and verification trilogy for model checking real systems under development. In this paper we assume there are no hardware failures or lost messages. As the AAC design develops and hardware details are decided by AAC designers, we plan to take the failure rates of the chosen components into consideration, i.e. by extending our work to probabilistic model checking using PRISM [19]. Previous work has reported on analyzing the safety of air traffic control systems using simulation [3] or fault trees [1]. By extending the model we designed in this paper, we can carry out safety analysis using PRISM to capture the dynamic interactions in the AAC.
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.