Artifact to supplement the paper: The VerCors Verifier: a Progress Report

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 theVerCors verifier. VerCors supports deductive verification ofconcurrent software, written in multiple programming languages, wherethe specifications are written in terms of pre-/postconditioncontracts using permission-based separation logic. In essence, VerCorsis a program transformation tool: it translates an annotated programinto input for the Viper framework, which is then used as verificationback-end. The paper discussesthe different programming languages and features for which VerCors providesverification support. It also discusses how the tool internally hasbeen reorganised to become easily extendible, and to improve the connectionand interaction with Viper. In addition, we also introduce two toolsbuilt on top of VerCors, which support correctness-preserving transformations ofverified programs. Finally, we discuss how the VerCors verifier hasbeen used on a range of realistic case studies.