Here you can find some further material about the talk "Concurrency Correctness Witnesses with Ghosts" at the 1st Workshop on Verification Witnesses and Their Validation (VeWit 2023). In this talk we pursue to improve the format for concurrency correctness witnesses with the introduction of ghost variables.
This repository contains the following materials:
-
The abstract submitted to the workshop
-
The slides of the talk
-
The examples shown in the talk as proper C-programs. The folder contains the original program, the YAML-witness and the program that corresponds to this witness (by instrumenting the program with data from the witness, such as ghost variables).
-
The YAML schema of the witness proposal
-
The documentation generated from the schema. The rendered HTML can be seen here.
-
The tools to check the examples and generate the documentation on your own. Further documentation can be found here.