The VerCors Verifier: A Progress Report

Lukas Armborst; Pieter Bos; Lars B. van den Haak; Marieke Huisman; Robert Rubbens; Ömer Şakar; Philip Tasche

doi:10.1007/978-3-031-65630-9_1

The VerCors Verifier: A Progress Report

Lukas Armborst, Pieter Bos, Lars B. van den Haak, Marieke Huisman, Robert Rubbens^*, Ömer Şakar, Philip Tasche

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

1 Citation (Scopus)

37 Downloads (Pure)

Abstract

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.

Original language	English
Title of host publication	Computer Aided Verification - 36th International Conference, CAV 2024, Proceedings
Subtitle of host publication	36th International Conference on Computer Aided Verification
Editors	Arie Gurfinkel, Vijay Ganesh
Publisher	Springer
Pages	3-18
Number of pages	16
Volume	2
ISBN (Electronic)	978-3-031-65630-9
ISBN (Print)	978-3-031-65629-3
DOIs	https://doi.org/10.1007/978-3-031-65630-9_1
Publication status	Published - 2024

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	14682 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/978-3-031-65630-9_1Licence: CC BY

ArticleFinal published version, 364 KBLicence: CC BY

Cite this

Armborst, L., Bos, P., van den Haak, L. B., Huisman, M., Rubbens, R., Şakar, Ö., & Tasche, P. (2024). The VerCors Verifier: A Progress Report. In A. Gurfinkel, & V. Ganesh (Eds.), Computer Aided Verification - 36th International Conference, CAV 2024, Proceedings: 36th International Conference on Computer Aided Verification (Vol. 2, pp. 3-18). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14682 LNCS). Springer. https://doi.org/10.1007/978-3-031-65630-9_1

Armborst, Lukas ; Bos, Pieter ; van den Haak, Lars B. et al. / The VerCors Verifier : A Progress Report. Computer Aided Verification - 36th International Conference, CAV 2024, Proceedings: 36th International Conference on Computer Aided Verification. editor / Arie Gurfinkel ; Vijay Ganesh. Vol. 2 Springer, 2024. pp. 3-18 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{57e1419b059441b3a13884119e5e2a8e,

title = "The VerCors Verifier: A Progress Report",

abstract = "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.",

author = "Lukas Armborst and Pieter Bos and {van den Haak}, {Lars B.} and Marieke Huisman and Robert Rubbens and {\"O}mer {\c S}akar and Philip Tasche",

note = "Publisher Copyright: {\textcopyright} The Author(s) 2024.",

year = "2024",

doi = "10.1007/978-3-031-65630-9_1",

language = "English",

isbn = "978-3-031-65629-3",

volume = "2",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "3--18",

editor = "Arie Gurfinkel and Vijay Ganesh",

booktitle = "Computer Aided Verification - 36th International Conference, CAV 2024, Proceedings",

address = "Germany",

}

Armborst, L, Bos, P, van den Haak, LB, Huisman, M , Rubbens, R, Şakar, Ö & Tasche, P 2024, The VerCors Verifier: A Progress Report. in A Gurfinkel & V Ganesh (eds), Computer Aided Verification - 36th International Conference, CAV 2024, Proceedings: 36th International Conference on Computer Aided Verification. vol. 2, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14682 LNCS, Springer, pp. 3-18. https://doi.org/10.1007/978-3-031-65630-9_1

The VerCors Verifier: A Progress Report. / Armborst, Lukas; Bos, Pieter; van den Haak, Lars B. et al.
Computer Aided Verification - 36th International Conference, CAV 2024, Proceedings: 36th International Conference on Computer Aided Verification. ed. / Arie Gurfinkel; Vijay Ganesh. Vol. 2 Springer, 2024. p. 3-18 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14682 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - The VerCors Verifier

T2 - A Progress Report

AU - Armborst, Lukas

AU - Bos, Pieter

AU - van den Haak, Lars B.

AU - Huisman, Marieke

AU - Rubbens, Robert

AU - Şakar, Ömer

AU - Tasche, Philip

PY - 2024

Y1 - 2024

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85200655070&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-65630-9_1

DO - 10.1007/978-3-031-65630-9_1

M3 - Conference contribution

SN - 978-3-031-65629-3

VL - 2

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 3

EP - 18

BT - Computer Aided Verification - 36th International Conference, CAV 2024, Proceedings

A2 - Gurfinkel, Arie

A2 - Ganesh, Vijay

PB - Springer

ER -

Armborst L, Bos P, van den Haak LB, Huisman M , Rubbens R, Şakar Ö et al. The VerCors Verifier: A Progress Report. In Gurfinkel A, Ganesh V, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Proceedings: 36th International Conference on Computer Aided Verification. Vol. 2. Springer. 2024. p. 3-18. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-65630-9_1

The VerCors Verifier: A Progress Report

Abstract

Publication series

Access to Document

Other files and links

Fingerprint

Cite this