Armborst, Lukas; Bos, Pieter; van den Haak, Lars; Huisman, Marieke; Rubbens, Robert et. al. (2024): Artifact to supplement the paper: The VerCors Verifier: a Progress Report. Version 1. 4TU.ResearchData. dataset. https://doi.org/10.4121/a5f97e07-9f84-4223-b581-6d2606fe07ba.v1

Dataset

x choose version: version 3 - 2024-08-01 (latest) version 2 - 2024-04-21

• Communications Technologies
• Technology

Alpinist, Deductive Verification, VCLLVM, VerCors, VeSUV, VeyMont

MPL 2.0

RefWorks, BibTeX, Reference Manager, Endnote, DataCite, NLM, DC, CFF

by Lukas Armborst , Pieter Bos , Lars van den Haak , Marieke Huisman , Robert Rubbens , Ömer Şakar , Philip Tasche

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.

• 2024-04-10 first online, published, posted

4TU.ResearchData

application/zip

• Mercedes: Maximal Reliability of Concurrent and Distributed Software (grant code 639.023.710) [more info...] Dutch Research Council
• ChEOPS (NWO TTW grant 17249)

University of Twente, Faculty of Electrical Engineering, Mathematics and Computer Science
Eindhoven University of Technology, Department of Mathematics and Computer Science