Evaluation of Specification Inference Tools for Deductive Verification

doi: 10.4121/9c83933e-8406-4e49-ac4d-1f8bb55ed988.v1
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
Datacite citation style:
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
Other citation styles (APA, Harvard, MLA, Vancouver, Chicago, IEEE) available at Datacite
Dataset

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.

history
  • 2023-06-19 first online, published, posted
publisher
4TU.ResearchData
format
Virtual Machines (.ova format), Markdown (.md) files, ZIP file containing .java, .html, .txt and .md files
funding
  • Mercedes: Maximal Reliability of Concurrent and Distributed Software (grant code 639.023.710) [more info...] Dutch Research Council
organizations
University of Twente, Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS), Formal Methods and Tools

DATA

files (4)