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

Artifact to supplement "The VerCors Verifier: a Progress Report;" Accepted at CAV 2024.<br>PAPER ABSTRACT<br>This paper gives an overview of the most recent developments on theVerCors verifier. VerCors supports deductive verification ofconcurrent software, written in multiple programming languages, wherethe specifications are written in terms of pre-/postconditioncontracts using permission-based separation logic. In essence, VerCorsis a program transformation tool: it translates an annotated programinto input for the Viper framework, which is then used as verificationback-end. The paper discussesthe different programming languages and features for which VerCors providesverification support. It also discusses how the tool internally hasbeen reorganised to become easily extendible, and to improve the connectionand interaction with Viper. In addition, we also introduce two toolsbuilt on top of VerCors, which support correctness-preserving transformations ofverified programs. Finally, we discuss how the VerCors verifier hasbeen used on a range of realistic case studies.<br>

用于补充《VerCors验证器：进展报告》的辅助材料，该论文已被CAV 2024收录。
论文摘要
本文概述了VerCors验证器的最新研发进展。VerCors支持对多种编程语言编写的并发软件进行演绎验证（deductive verification），其规格说明采用基于权限的分离逻辑（permission-based separation logic），以前置/后置条件契约（pre-/postcondition contracts）的形式撰写。本质上，VerCors是一款程序转换工具（program transformation tool）：它将带注释的程序转换为Viper框架（Viper framework）的输入，并以Viper作为验证后端（verification back-end）。本文讨论了VerCors支持验证的各类编程语言及其特性，同时阐述了该工具的内部重构方案，使其具备良好的可扩展性，并优化了与Viper框架的连接与交互机制。除此之外，本文还介绍了两款基于VerCors开发的工具，它们可对已验证程序进行保持正确性的转换（correctness-preserving transformations）操作。最后，本文探讨了VerCors验证器在一系列实际案例研究中的应用情况。