cff-version: 1.2.0 abstract: "

Artifact to supplement "The VerCors Verifier: a Progress Report;" Accepted at CAV 2024.


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.


" 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