Evaluation of Specification Inference Tools for Deductive Verification

About this artifactAs 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 informationThe tools are shared under their original licenses which are included in the dataset.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.