Artifact to supplement the tool-paper: Spectral - Translating Specifications for Deductive Verification into LLVM-IR

This artifact accompanies the paper “Spectral - Translating Specifications for Deductive Verification into LLVM-IR” which introduces Spectral, a tool that translates specifications from the level of different LLVM based source languages to LLVM-IR. Spectral currently supports specifications for subsets of C, C++ and Swift.

This artifact contains the source code of Spectral and the source code of the version of VerCors that has been extended to support Spectral’s specification format. Additionally, the examples that are used in the evaluation of the paper are included. The provided docker image contains executable versions of Spectral and VerCors along with scripts that can be used to replicate the experiments of the paper’s evaluation section (Tables 2 and 3). Additionally, the provided source code of Spectral contains documentation on how to build, use and extend Spectral.