Powered by OpenAIRE graph
Found an issue? Give us feedback
addClaim

This Research product is the result of merged Research products in OpenAIRE.

You have already added 0 works in your ORCID record related to the merged Research product.

Artifact for the VMCAI'2025 Paper "Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts"

Authors: Erhard, Julian; Bentele, Manuel; Heizmann, Matthias; Klumpp, Dominik; Saan, Simmo; Schüssele, Frank; Schwarz, Michael; +3 Authors

Artifact for the VMCAI'2025 Paper "Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts"

Abstract

This artifact allows for analysis and replication of the experimental results discussed in the paper"Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts". The paper describes ghost witnesses, an exchange format between verification tools for concurrentprograms. The artifact contains two such verification tools, Goblint and Ultimate GemCutter, as well asan experimental setup to evaluate the information exchange between these two tools. In particular, this artifact contains the following components: EVALUATION RESULTS :: The evaluation results, and overview tables (HTML) generated from the raw data. 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 :: The benchmarks used for evaluation of the verifiers. BENCHMARK WITNESSES :: The witnesses generated by Goblint, which were used in the experiments. BENCHEXEC TOOL :: The BenchExec benchmarking tool can be used to replicate our results. The artifact consists of a virtual machine (rather than a docker image), as we use the benchmarking toolBenchExec which itself relies on containerization and cannot easily be run inside a container.The virtual machine was created on Linux Ubuntu.

Related Organizations
Keywords

Software Verification, Correctness Witnesses, Ghost Variables, Abstract Interpretation, Concurrency, Model Checking

  • BIP!
    Impact byBIP!
    selected citations
    These citations are derived from selected sources.
    This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    1
    popularity
    This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
    Average
    influence
    This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    Average
    impulse
    This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
    Average
Powered by OpenAIRE graph
Found an issue? Give us feedback
selected citations
These citations are derived from selected sources.
This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Citations provided by BIP!
popularity
This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
BIP!Popularity provided by BIP!
influence
This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Influence provided by BIP!
impulse
This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
BIP!Impulse provided by BIP!
1
Average
Average
Average