cff-version: 1.2.0
abstract: "<p><strong>About this artifact</strong></p><p>As part of our research, we evaluated the impact of several specification inference tools for deductive verification.</p><p>This artifact contains the following things:</p><p>- 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.</p><p>- Strongarm.ova: A Virtual Machine with the tool Strongarm installed. It also contains the examples we used to test the tool.</p><p>- 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.</p><p><br></p><p>You can use the Virtual Machines to try the specification inference tools yourself.</p><p>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.</p><p><br></p><p><strong>License information</strong></p><p>The tools are shared under their original licenses.</p><p>The ArrayList.java and Counter.java examples are licensed under CC-BY 4.0.</p><p>The BinarySearchGood.java example is originally from https://www.openjml.org/examples and is shared under the CC-BY-NC 4.0 license.</p>"
authors:
  - family-names: Lathouwers
    given-names: Sophie
    orcid: "https://orcid.org/0000-0002-7544-447X"
  - family-names: Huisman
    given-names: Marieke
    orcid: "https://orcid.org/0000-0003-4467-072X"
title: "Evaluation of Specification Inference Tools for Deductive Verification"
keywords:
version: 1
identifiers:
  - type: doi
    value: 10.4121/9c83933e-8406-4e49-ac4d-1f8bb55ed988.v1
license: CC BY 4.0
date-released: 2023-06-19