diff --git a/docs/artifact-descriptions/vmcai25.md b/docs/artifact-descriptions/vmcai25.md index ac9312caa8..9f2de1c511 100644 --- a/docs/artifact-descriptions/vmcai25.md +++ b/docs/artifact-descriptions/vmcai25.md @@ -9,20 +9,20 @@ The artifact contains [Goblint at `vmcai25` git tag](https://github.com/goblint/ ------------------------------------------------------------------------------- -## OVERVIEW +## Overview This artifact contains the following components: - EVALUATION RESULTS :: The evaluation results, and overview tables (HTML) + Evaluation Results :: The evaluation results, and overview tables (HTML) generated from the raw data. - SOURCE CODE :: Source code for Goblint and Ultimate GemCutter, + Source Code :: Source code for Goblint and Ultimate GemCutter, the verification tools used in the experiments for the paper. - VERIFIER BINARIES :: Binaries for Goblint and Ultimate GemCutter. - BENCHMARK PROGRAMS :: Benchmarks used for evaluation of the verifiers. - BENCHMARK WITNESSES :: The witnesses generated by Goblint, as used in the + Verifier Binaries :: Binaries for Goblint and Ultimate GemCutter. + Benchmark Programs :: Benchmarks used for evaluation of the verifiers. + Benchmark Witnesses :: The witnesses generated by Goblint, as used in the experiments. - BENCHEXEC TOOL :: The BenchExec benchmarking tool can be used + BenchExec Tool :: The BenchExec benchmarking tool can be used to replicate our results on these benchmarks. The next section gives instructions on how to setup and quickly get an overview of the artifact. @@ -31,7 +31,7 @@ The final section gives information on how to reuse this artifact. ------------------------------------------------------------------------------- -## GETTING STARTED +## Getting Started ### 1. Setup @@ -67,7 +67,7 @@ The times for the Table 2 are given first in seconds and then pretty-printed as For a more detailed inspection and visualization of the data, take a look at the generated HTML report. Just open the file `~/witness-validation/paper-evaluation/results.2024-09-24_22-00-48.table.html` in firefox. -For detailed information, see the "EVALUATION RESULTS" section below. +For detailed information, see the "Evaluation Results" section below. ### 3. Quick Test of the Benchmark Setup @@ -192,7 +192,7 @@ Naturally, changes to the timeout or memory are expected to affect the evaluatio ---------------------------------------------------------------------------------- -## EVALUATION RESULTS +## Evaluation Results The evaluation results that form the basis for the experimental data in the paper can be found in the directory `~/witness-validation/paper-evaluation/`. The witnesses generated by Goblint that formed the basis for this evaluation can be found in `~/witness-generation/paper-evaluation/`. @@ -228,7 +228,7 @@ As described above (in section _2. Inspect the evaluation results_), the artifac ---------------------------------------------------------------------------------- -## SOURCE CODE +## Source Code ### GemCutter @@ -257,7 +257,7 @@ More recent versions of Goblint can be found at . ---------------------------------------------------------------------------------- -## VERIFIER BINARIES +## Verifier Binaries A pre-built binary of GemCutter can be found in `~/ultimate/releaseScripts/default/UGemCutter-linux/`. For information on how to execute GemCutter, consult the `README` in `~/ultimate/releaseScripts/default/UGemCutter-linux/`. @@ -272,7 +272,7 @@ For examples, see the benchmark definition files `~/witness-generation/goblint.x ---------------------------------------------------------------------------------- -## BENCHMARK PROGRAMS +## Benchmark Programs This artifact includes the benchmark programs on which we evaluated the verifiers. These benchmarks are taken from the publicly available sv-benchmarks set () @@ -281,7 +281,7 @@ The benchmarks are written in C and use POSIX threads (`pthreads`) to model conc ---------------------------------------------------------------------------------- -## EXTENDING & REUSING THIS ARTIFACT +## Extending & Reusing This Artifact * **Building a modified version of the VM:** This VM was created using the `vagrant` tool (). The `Vagrantfile` used to build the artifact, along with several other files used in the build, is included in the directory `~/artifact`.