Updates v2

aman-goel · Nov 8, 2019 · dc8e11e · dc8e11e
1 parent 8dcdaee
commit dc8e11e
Showing 1 changed file with 90 additions and 2 deletions.
diff --git a/Readme.txt b/Readme.txt
@@ -28,7 +28,8 @@ Includes experimental evaluation of :
 -> certificates                         (Section 3.2)       (Experiment 1-12)
 -> proof race                           (Section 3.3)       (Experiment 10-11)
 
-Check the License.txt for license information.
+For details on what each experiment is trying to evaluate, 
+refer to the Detailed description section in this file at the end.
 
 The tool is available on github - https://github.com/aman-goel/avr
 The artifact is maintained on github - https://github.com/aman-goel/tacas20ae
@@ -49,6 +50,93 @@ The script run.sh goes through each experiment interactively, and prints further
 on what part of the paper is the experiment trying to evaluate.
 You need to press enter before and after running each experiment (as displayed by run.sh).
 
-The file avr/expected_results.zip contains the expected log of running run.sh (generated on TACAS 2020 VM).
+The file avr/expected_results.zip contains the expected log of running run.sh 
+(generated on TACAS 2020 VM).
+
+--------------------------------------------------------------------------
+Detailed description (of each experiment)
+--------------------------------------------------------------------------
+Experiment 1-
+  evaluates: 
+    first case study (part 1)              (Section 4.1) 
+    VMT frontend                           (Section 3) 
+    proof certificates                     (Section 3.2)
+    verifying certificates using yices2    (Section 3.2)
+
+Experiment 2-
+  evaluates: 
+    first case study (part 1)              (Section 4.1) 
+    VMT frontend                           (Section 3) 
+    proof certificates                     (Section 3.2)
+    verifying certificates using z3        (Section 3.2)
+
+Experiment 3-
+  evaluates: 
+    first case study (part 2)              (Section 4.1) 
+    VMT frontend                           (Section 3) 
+    proof certificates                     (Section 3.2)
+    verifying certificates using yices2    (Section 3.2)
+
+Experiment 4-
+  evaluates: 
+    first case study (part 2)              (Section 4.1) 
+    VMT frontend                           (Section 3) 
+    proof certificates                     (Section 3.2)
+    verifying certificates using mathsat   (Section 3.2)
+
+Experiment 5-
+  evaluates: 
+    second case study                      (Section 4.2) 
+    BTOR2 frontend                         (Section 3) 
+    counterexample traces                  (Section 3.2)
+    verifying certificates using BtorSIM   (Section 3.2)
+
+Experiment 6-
+  evaluates: 
+    second case study                      (Section 4.2) 
+    BTOR2 frontend                         (Section 3) 
+    counterexample traces                  (Section 3.2)
+    verifying certificates using BtorSIM   (Section 3.2)
+
+Experiment 7-
+  evaluates: 
+    verifying distributed protocols        (Section 5.1) 
+    BTOR2 frontend                         (Section 3) 
+    proof certificates                     (Section 3.2)
+    verifying certificates using yices2    (Section 3.2)
+
+Experiment 8-
+  evaluates: 
+    verifying distributed protocols        (Section 5.1) 
+    BTOR2 frontend                         (Section 3) 
+    proof certificates                     (Section 3.2)
+    verifying certificates using yices2    (Section 3.2)
+
+Experiment 9-
+  evaluates: 
+    Verilog frontend                       (Section 3) 
+
+Experiment 10-
+  evaluates: 
+    different techniques and add-ons       (Section 3.1) 
+    Verilog frontend                       (Section 3) 
+    proof race                             (Section 3.3)
+    proof certificates                     (Section 3.2)
+    verifying certificates using yices2    (Section 3.2)
+
+Experiment 11-
+  evaluates: 
+    different techniques and add-ons       (Section 3.1) 
+    Verilog frontend                       (Section 3) 
+    proof race                             (Section 3.3)
+    proof certificates                     (Section 3.2)
+    verifying certificates using yices2    (Section 3.2)
+
+Experiment 12-
+  evaluates: 
+    utilities                              (Section 3.1) 
+    Verilog frontend                       (Section 3) 
+    proof certificates                     (Section 3.2)
+    verifying certificates using yices2    (Section 3.2)
 
 Thank you, and please let the authors know in the case of any difficulty.