Skip to content

Commit

Permalink
Fix lists in VMACI24 artifact description
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Jan 23, 2024
1 parent 380979e commit 3625b67
Showing 1 changed file with 22 additions and 19 deletions.
41 changes: 22 additions & 19 deletions docs/artifact-descriptions/vmcai24.md
Original file line number Diff line number Diff line change
Expand Up @@ -17,13 +17,14 @@ This artifact contains everything mentioned in the evaluation section of the pap
* `LICENSE`.
* `unassume.ova` — VirtualBox virtual machine.

In `/home/vagrant` contains:
* `goblint/` ­— Goblint with unassume support, including source code.
* `CPAchecker-2.2-unix/` — CPAchecker from [SV-COMP 2023 archives](https://gitlab.com/sosy-lab/sv-comp/archives-2023).
* `UAutomizer-linux/` — Ultimate Automizer from [SV-COMP 2023 archives](https://gitlab.com/sosy-lab/sv-comp/archives-2023).
* `eval-prec/` — precision evaluation (script, benchmarks, manual witnesses).
* `eval-perf/` — performance evaluation (script, benchmarks, manual witnesses).
* `results/` — results (initially empty).
In `/home/vagrant` contains:

* `goblint/` ­— Goblint with unassume support, including source code.
* `CPAchecker-2.2-unix/` — CPAchecker from [SV-COMP 2023 archives](https://gitlab.com/sosy-lab/sv-comp/archives-2023).
* `UAutomizer-linux/` — Ultimate Automizer from [SV-COMP 2023 archives](https://gitlab.com/sosy-lab/sv-comp/archives-2023).
* `eval-prec/` — precision evaluation (script, benchmarks, manual witnesses).
* `eval-perf/` — performance evaluation (script, benchmarks, manual witnesses).
* `results/` — results (initially empty).

* `results/` — evaluation results tables with data used for the paper.

Expand All @@ -36,25 +37,27 @@ This artifact contains everything mentioned in the evaluation section of the pap
1. Run `./eval-prec/run.sh` in the terminal emulator. This takes ~42min.
2. Run `firefox results/eval-prec/table-generator.table.html` to view the results.

The HTML table contains the following status columns (cputime, walltime and memory can be ignored):
1. Goblint w/o witness (true means verified).
2. Goblint w/ manual witness (true means witness validated).
3. Goblint w/ witness from CPAchecker (true means program verified with witness-guidance).
4. Goblint w/ witness from CPAchecker (true means witness validated).
5. Goblint w/ witness from UAutomizer (true means program verified with witness-guidance).
6. Goblint w/ witness from UAutomizer (true means witness validated).
The HTML table contains the following status columns (cputime, walltime and memory can be ignored):

1. Goblint w/o witness (true means verified).
2. Goblint w/ manual witness (true means witness validated).
3. Goblint w/ witness from CPAchecker (true means program verified with witness-guidance).
4. Goblint w/ witness from CPAchecker (true means witness validated).
5. Goblint w/ witness from UAutomizer (true means program verified with witness-guidance).
6. Goblint w/ witness from UAutomizer (true means witness validated).

Table 1 in the paper presents these results, except the rows are likely in a different order.

### Performance evaluation
1. Run `./eval-perf/run.sh` in the terminal emulator. This takes ~30s.
2. Run `firefox results/eval-perf/table-generator.table.html` to view the results.

The HTML table contains the following relevant columns (others can be ignored):
1. Goblint w/o witness, evals.
2. Goblint w/o witness, cputime.
3. Goblint w/ manual witness, evals.
4. Goblint w/ manual witness, cputime.
The HTML table contains the following relevant columns (others can be ignored):

1. Goblint w/o witness, evals.
2. Goblint w/o witness, cputime.
3. Goblint w/ manual witness, evals.
4. Goblint w/ manual witness, cputime.

Table 2 in the paper presents these results, except the rows are likely in a different order.

Expand Down

0 comments on commit 3625b67

Please sign in to comment.