@@ -17,13 +17,14 @@ This artifact contains everything mentioned in the evaluation section of the pap
17
17
* ` LICENSE ` .
18
18
* ` unassume.ova ` — VirtualBox virtual machine.
19
19
20
- In ` /home/vagrant ` contains:
21
- * ` goblint/ ` — Goblint with unassume support, including source code.
22
- * ` CPAchecker-2.2-unix/ ` — CPAchecker from [ SV-COMP 2023 archives] ( https://gitlab.com/sosy-lab/sv-comp/archives-2023 ) .
23
- * ` UAutomizer-linux/ ` — Ultimate Automizer from [ SV-COMP 2023 archives] ( https://gitlab.com/sosy-lab/sv-comp/archives-2023 ) .
24
- * ` eval-prec/ ` — precision evaluation (script, benchmarks, manual witnesses).
25
- * ` eval-perf/ ` — performance evaluation (script, benchmarks, manual witnesses).
26
- * ` results/ ` — results (initially empty).
20
+ In ` /home/vagrant ` contains:
21
+
22
+ * ` goblint/ ` — Goblint with unassume support, including source code.
23
+ * ` CPAchecker-2.2-unix/ ` — CPAchecker from [ SV-COMP 2023 archives] ( https://gitlab.com/sosy-lab/sv-comp/archives-2023 ) .
24
+ * ` UAutomizer-linux/ ` — Ultimate Automizer from [ SV-COMP 2023 archives] ( https://gitlab.com/sosy-lab/sv-comp/archives-2023 ) .
25
+ * ` eval-prec/ ` — precision evaluation (script, benchmarks, manual witnesses).
26
+ * ` eval-perf/ ` — performance evaluation (script, benchmarks, manual witnesses).
27
+ * ` results/ ` — results (initially empty).
27
28
28
29
* ` results/ ` — evaluation results tables with data used for the paper.
29
30
@@ -36,25 +37,27 @@ This artifact contains everything mentioned in the evaluation section of the pap
36
37
1 . Run ` ./eval-prec/run.sh ` in the terminal emulator. This takes ~ 42min.
37
38
2 . Run ` firefox results/eval-prec/table-generator.table.html ` to view the results.
38
39
39
- The HTML table contains the following status columns (cputime, walltime and memory can be ignored):
40
- 1 . Goblint w/o witness (true means verified).
41
- 2 . Goblint w/ manual witness (true means witness validated).
42
- 3 . Goblint w/ witness from CPAchecker (true means program verified with witness-guidance).
43
- 4 . Goblint w/ witness from CPAchecker (true means witness validated).
44
- 5 . Goblint w/ witness from UAutomizer (true means program verified with witness-guidance).
45
- 6 . Goblint w/ witness from UAutomizer (true means witness validated).
40
+ The HTML table contains the following status columns (cputime, walltime and memory can be ignored):
41
+
42
+ 1 . Goblint w/o witness (true means verified).
43
+ 2 . Goblint w/ manual witness (true means witness validated).
44
+ 3 . Goblint w/ witness from CPAchecker (true means program verified with witness-guidance).
45
+ 4 . Goblint w/ witness from CPAchecker (true means witness validated).
46
+ 5 . Goblint w/ witness from UAutomizer (true means program verified with witness-guidance).
47
+ 6 . Goblint w/ witness from UAutomizer (true means witness validated).
46
48
47
49
Table 1 in the paper presents these results, except the rows are likely in a different order.
48
50
49
51
### Performance evaluation
50
52
1 . Run ` ./eval-perf/run.sh ` in the terminal emulator. This takes ~ 30s.
51
53
2 . Run ` firefox results/eval-perf/table-generator.table.html ` to view the results.
52
54
53
- The HTML table contains the following relevant columns (others can be ignored):
54
- 1 . Goblint w/o witness, evals.
55
- 2 . Goblint w/o witness, cputime.
56
- 3 . Goblint w/ manual witness, evals.
57
- 4 . Goblint w/ manual witness, cputime.
55
+ The HTML table contains the following relevant columns (others can be ignored):
56
+
57
+ 1 . Goblint w/o witness, evals.
58
+ 2 . Goblint w/o witness, cputime.
59
+ 3 . Goblint w/ manual witness, evals.
60
+ 4 . Goblint w/ manual witness, cputime.
58
61
59
62
Table 2 in the paper presents these results, except the rows are likely in a different order.
60
63
0 commit comments