Evaluation Data of the Implementation of the Approach for Automatic Test Generation for Information-Flow Properties

This data set contains the programs for which the automatic test generation approach of the KeY theorem prover was used to automatically generate noninterference tests. The approach is described in http://dx.doi.org/10.1145/3297280.3297500 DATA<br> ---------<br> The data folder contains the secure and insecure programs which were evaluated and the tests which were generated for them. Each program is in the folder "program" and is written in Java and specified in an extended version of the JML specification language. Check out http://dx.doi.org/10.5445/IR/1000046878 for a reference on the used specification language. For each example we provide the tests that were generated. For the insecure examples we provide the tests generated with each of the two options of our approach. The tests generated with the option for searching for counterexamples is in the folder "WithPost" of each insecure example.