The folder structure in icse2022-subm-data-1008-orm-verification 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. The structure of folder src/ is as follows: -ControllerSummaryInference-src: Code for inferring relational-algebraic summaries of Spring-based web applications and alloy translation. -multipage-src: Code for checking trace properties. The file other-details.pdf contains syntax directed rules as well as loop patterns in tool which form the approach to infer relational summaries from ORM controllers.