cff-version: 1.2.0
abstract: "<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>"
authors:
  - family-names: Armborst
    given-names: Lukas
    orcid: "https://orcid.org/0000-0001-7565-0954"
  - family-names: Bos
    given-names: Pieter
    orcid: "https://orcid.org/0009-0003-0240-3305"
  - family-names: van den Haak
    given-names: Lars
    orcid: "https://orcid.org/0000-0002-0330-5016"
  - family-names: Huisman
    given-names: Marieke
    orcid: "https://orcid.org/0000-0003-4467-072X"
  - family-names: Rubbens
    given-names: Robert
    orcid: "https://orcid.org/0000-0002-5638-5945"
  - family-names: Şakar
    given-names: Ömer
    orcid: "https://orcid.org/0000-0003-3457-5446"
  - family-names: Tasche
    given-names: Philip
    orcid: "https://orcid.org/0000-0003-1518-4079"
title: "Artifact to supplement the paper: The VerCors Verifier: a Progress Report"
keywords:
version: 3
identifiers:
  - type: doi
    value: 10.4121/a5f97e07-9f84-4223-b581-6d2606fe07ba.v3
license: MPL 2.0
date-released: 2024-08-01