Artifact to supplement the paper: The VerCors Verifier: a Progress Report

doi:10.4121/a5f97e07-9f84-4223-b581-6d2606fe07ba.v3
The doi above is for this specific version of this dataset, which is currently the latest. Newer versions may be published in the future. For a link that will always point to the latest version, please use
doi: 10.4121/a5f97e07-9f84-4223-b581-6d2606fe07ba
Datacite citation style:
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 3. 4TU.ResearchData. dataset. https://doi.org/10.4121/a5f97e07-9f84-4223-b581-6d2606fe07ba.v3
Other citation styles (APA, Harvard, MLA, Vancouver, Chicago, IEEE) available at Datacite
Dataset
choose version:
version 3 - 2024-08-01 (latest)
version 2 - 2024-04-21 version 1 - 2024-04-10
University of Twente logo
usage stats
346
views
1096
downloads
licence
MPL 2.0

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.


history
  • 2024-04-10 first online
  • 2024-08-01 published, posted
publisher
4TU.ResearchData
format
application/zip
associated peer-reviewed publication
The VerCors Verifier: a Progress Report
funding
  • Mercedes: Maximal Reliability of Concurrent and Distributed Software (grant code 639.023.710) [more info...] Dutch Research Council
  • ChEOPS (NWO TTW grant 17249)
organizations
University of Twente, Faculty of Electrical Engineering, Mathematics and Computer Science
Eindhoven University of Technology, Department of Mathematics and Computer Science

DATA

files (1)