Verification of ORM-based Controllers by Summary Inference

Submission data for  ICSE 2022 Verification of ORM-based Controllers by Summary Inference.

The folder structure in this repository is as follows. 

ControllerVerificationData contains results corresponding to Section 5.2 of
the paper. The folder hierarchy within this is:

    benchmark name ->

      Controller class name ->

        "Alloy" ->

          a .als file (i.e., Alloy model/summary generated by our tool)
          corresponding to each controller method, with assertions added
          manually in all cases were they were expressible.

        "Output" -> outputs from Alloy for the assertions.

multipage-data contains results corresponding to Section 5.3 of the paper.

  "properties" ->

     each .txt file contains a property (basically, a \psi as in Section
     3.1 in the paper), written by us, in Alloy form. (For "Unexpressed"
     properties, we wrote a dummy property.)

  "toCheck" ->

     a property number ->

      Generated Alloy files for this property (one Alloy file for Property
      (A) and one each for Property (I), see Section 3.1 in the paper)

      A .txt file for each Alloy file, containing Alloy checker's output.

   "summary.txt" contains a summary of all the information above

Mutation-Analysis contains results corresponding to Section 5.5 of the
paper.

  Each leaf level folder under this contains:

   Alloy file generated for a mutated version of the benchmark, with
   assertions added manually.

   The description of the mutation (in the .desc file)

   A .out file containing output from the Alloy checker for the assertions
   in the .als file. 

JPF contains results corresponding to Section 5.6 of the paper. 

  Each leaf-level folder contains results pertaining to one of the 16
  assertions. The .java file contains a driver that initializes the tables,
  calls the controller, and checks the assertion. The .jpf file is required
  by JPF, and the .out file shows the JPF output. 

We will positively consider taking steps to make our tool open-source in
the near future. As of today there are some licensing issues due to our
dependence on DBridge source.