Merge pull request #1332 from goblint/unassume-artifact

Add VMCAI '24 artifact description to docs

Author: sim642

docs/artifact-descriptions/vmcai24.md

@@ -0,0 +1,83 @@
+# VMCAI '24 Artifact Description
+## Correctness Witness Validation by Abstract Interpretation
+
+This is the artifact description for our [VMCAI '24 paper "Correctness Witness Validation by Abstract Interpretation"](https://doi.org/10.1007/978-3-031-50524-9_4).
+The artifact is available on [Zenodo](https://doi.org/10.5281/zenodo.8253000).
+
+This artifact contains everything mentioned in the evaluation section of the paper: Goblint implementation, scripts, benchmarks, manual witnesses and other tools.
+
+**The description here is provided for convenience and not maintained.**
+The artifact is based on [Goblint at `vmcai24` git tag](https://github.com/goblint/analyzer/releases/tag/vmcai24) and [Goblint benchmarks at `vmcai24` git tag](https://github.com/goblint/bench/releases/tag/vmcai24).
+
+## Requirements
+* [VirtualBox](https://www.virtualbox.org/).
+* 2 CPU cores.
+* 8 GB RAM.
+* 7 GB disk space.
+* ~45min.
+
+## Layout
+* `README.md`/`README.pdf` — this file.
+* `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).
+
+* `results/` — evaluation results tables with data used for the paper.
+
+## Reproduction
+1. Import the virtual machine into VirtualBox.
+2. Start the virtual machine and log in with username "vagrant" (not "Ubuntu"!) and password "vagrant".
+3. Right click on the desktop and open Applications → Accessories → Terminal Emulator.
+
+### Precision evaluation
+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).
+
+   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.
+
+   Table 2 in the paper presents these results, except the rows are likely in a different order.
+
+
+## Goblint implementation
+[Goblint](https://github.com/goblint/analyzer) is an open source static analysis framework for C.
+Goblint itself is written in OCaml.
+Being open source, it allows existing implementations of analyses and abstract domains to be reused and modified.
+As a framework, it also allows new ones to be easily added.
+For more details, refer to the linked GitHub repository and related documentation.
+
+Key parts of the code related to this paper are the following:
+
+1. `src/analyses/unassumeAnalysis.ml`: analysis, which emits unassume operation events to other analyses for YAML-witness–guided verification.
+2. `src/analyses/base.ml` lines 2551–2641: propagating unassume for non-relational domains of the `base` analysis.
+3. `src/analyses/apron/relationAnalysis.apron.ml` lines 668–693: strengthening-based dual-narrowing unassume for relational Apron domains of the `apron` analysis.
+4. `src/cdomains/apron/apronDomain.apron.ml` lines 625–679: strengthening operator used for dual-narrowing of Apron domains.
+5. `src/util/wideningTokens.ml`: analysis lifter that adds widening tokens for delaying widenings from unassuming.
+6. `src/witness/yamlWitness.ml` lines 398–683: YAML witness validation.

mkdocs.yml

@@ -39,3 +39,4 @@ nav:
   - '📦 Artifact descriptions':
     - "🇸 SAS '21": artifact-descriptions/sas21.md
     - "🇪 ESOP '23": artifact-descriptions/esop23.md
+    - "🇻 VMCAI '24": artifact-descriptions/vmcai24.md