Artifact to supplement "The VerCors Verifier: a Progress Report"
Conditionally accepted at CAV 2024 pending evaluation of this artifact.
PAPER ABSTRACT
This paper gives an overview of the most recent developments on the
VerCors verifier. VerCors supports deductive verification of
concurrent software, written in multiple programming languages, where
the specifications are written in terms of pre-/postcondition
contracts using permission-based separation logic. In essence, VerCors
is a program transformation tool: it translates an annotated program
into input for the Viper framework, which is then used as verification
back-end. The paper discusses
the different programming languages and features for which VerCors provides
verification support. It also discusses how the tool internally has
been reorganised to become easily extendible, and to improve the connection
and interaction with Viper. In addition, we also introduce two tools
built on top of VerCors, which support correctness-preserving transformations of
verified programs. Finally, we discuss how the VerCors verifier has
been used on a range of realistic case studies.