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 -

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.


ER -