The doi above is for this specific version of this dataset, which is currently the latest. Newer versions may be published in the future. For a link that will always point to the latest version, please use
doi: 10.4121/9c83933e-8406-4e49-ac4d-1f8bb55ed988

Lathouwers, Sophie; Huisman, Marieke (2023): Evaluation of Specification Inference Tools for Deductive Verification. Version 1. 4TU.ResearchData. dataset. https://doi.org/10.4121/9c83933e-8406-4e49-ac4d-1f8bb55ed988.v1

Dataset

• Computer Software
• Information and Computing Sciences

Annotations, Deductive verification, Specification generation, Specification inference, Specifications

CC BY 4.0

RefWorks, BibTeX, Reference Manager, Endnote, DataCite, NLM, DC, CFF

by Sophie Lathouwers , Marieke Huisman

About this artifact

As part of our research, we evaluated the impact of several specification inference tools for deductive verification.

This artifact contains the following things:

- input-output-examples-for-specification-inference/: A directory containing the inputs we used to test specification inference tools as well as the output that the tools ChatGPT, Daikon, EvoSpex, Strongarm and Toradocu generated.

- Strongarm.ova: A Virtual Machine with the tool Strongarm installed. It also contains the examples we used to test the tool.

- SpecInferenceSurveyArtifact.ova: A Virtual Machine with the tools Daikon, EvoSpex and Toradocu installed. It also contains the code, documentation and a test suite for the examples we used to test the tools.

You can use the Virtual Machines to try the specification inference tools yourself.

If you're only interested in the input/output we used for testing the tools, then the input-output-examples-for-specification-inference/ directory should be sufficient.

License information

The tools are shared under their original licenses.

The ArrayList.java and Counter.java examples are licensed under CC-BY 4.0.

The BinarySearchGood.java example is originally from https://www.openjml.org/examples and is shared under the CC-BY-NC 4.0 license.

• 2023-06-19 first online, published, posted

4TU.ResearchData

Virtual Machines (.ova format), Markdown (.md) files, ZIP file containing .java, .html, .txt and .md files

• Mercedes: Maximal Reliability of Concurrent and Distributed Software (grant code 639.023.710) [more info...] Dutch Research Council

University of Twente, Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS), Formal Methods and Tools