%0 Generic
%A Lathouwers, Sophie
%A Huisman, Marieke
%D 2023
%T Evaluation of Specification Inference Tools for Deductive Verification
%U 
%R 10.4121/9c83933e-8406-4e49-ac4d-1f8bb55ed988.v1
%K Deductive verification
%K Specifications
%K Annotations
%K Specification inference
%K Specification generation
%X <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>
%I 4TU.ResearchData