The VerCors Verifier: A Progress Report
Formal Methods and Tools, University of Twente, Enschede, The Netherlands
Computer Aided Verification (CAV 2024), 2024
@inproceedings{armborst2024vercors,
title={The VerCors Verifier: A Progress Report},
author={Armborst, Lukas and Bos, Pieter and van den Haak, Lars B and Huisman, Marieke and Rubbens, Robert and {c{S}}akar, {"O}mer and Tasche, Philip},
booktitle={International Conference on Computer Aided Verification},
pages={3–18},
year={2024},
organization={Springer}
}
This paper gives an overview of the most recent developments on the VerCors verifier. VerCors is a deductive verifier for 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.
August 18, 2024 by hgpu
