Database of Annotations for Deductive Verifiers

This dataset was set up as part of our research titled "Formal Specifications Investigated: A Classification and Analysis of Annotations for Deductive Verifiers". It contains <b>a large set of annotations</b> that were classified according to our taxonomy. We also include the information we used to calculate the confidence intervals that are reported in the paper in Section 4.<br><br>The annotations were extracted from examples and case studies for the tools <b>KeY, Krakatoa, OpenJML, VerCors</b> and <b>Verifast</b>. We have included the 10 examples per tool (case studies are not included) from which these annotations have been extracted in <i>sample-sources.zip</i>. These are <b>not</b> licensed under the CC BY 4.0 but under their original licenses. These licenses have been included.<br><br>The README.md explains what the different files are.<br>