%0 Generic
%A Armborst, Lukas
%A Bos, Pieter
%A van den Haak, Lars
%A Huisman, Marieke
%A Rubbens, Robert
%A Şakar, Ömer
%A Tasche, Philip
%D 2024
%T Artifact to supplement the paper: The VerCors Verifier: a Progress Report
%U 
%R 10.4121/a5f97e07-9f84-4223-b581-6d2606fe07ba.v3
%K Deductive Verification
%K VerCors
%K VCLLVM
%K Alpinist
%K VeSUV
%K VeyMont
%X <p>Artifact to supplement "The VerCors Verifier: a Progress Report;" Accepted at CAV 2024.</p><p><br></p><p>PAPER ABSTRACT</p><p><br></p><p>This paper gives an overview of the most recent developments on the</p><p>VerCors verifier. VerCors supports deductive verification of</p><p>concurrent software, written in multiple programming languages, where</p><p>the specifications are written in terms of pre-/postcondition</p><p>contracts using permission-based separation logic. In essence, VerCors</p><p>is a program transformation tool: it translates an annotated program</p><p>into input for the Viper framework, which is then used as verification</p><p>back-end. The paper discusses</p><p>the different programming languages and features for which VerCors provides</p><p>verification support. It also discusses how the tool internally has</p><p>been reorganised to become easily extendible, and to improve the connection</p><p>and interaction with Viper. In addition, we also introduce two tools</p><p>built on top of VerCors, which support correctness-preserving transformations of</p><p>verified programs. Finally, we discuss how the VerCors verifier has</p><p>been used on a range of realistic case studies.</p><p><br></p>
%I 4TU.ResearchData