TY - DATA
T1 - Artifact to supplement the paper: The VerCors Verifier: a Progress Report
PY - 2024/04/21
AU - Lukas Armborst
AU - Pieter Bos
AU - Lars van den Haak
AU - Marieke Huisman
AU - Robert Rubbens
AU - Ömer Şakar
AU - Philip Tasche
UR - 
DO - 10.4121/a5f97e07-9f84-4223-b581-6d2606fe07ba.v2
KW - Deductive Verification
KW - VerCors
KW - VCLLVM
KW - Alpinist
KW - VeSUV
KW - VeyMont
N2 - <p>Artifact to supplement "The VerCors Verifier: a Progress Report"</p><p>Conditionally accepted at CAV 2024 pending evaluation of this artifact.</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>
ER -