@InProceedings{Armborst24,
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",
editor="Gurfinkel, Arie
and Ganesh, Vijay",
title="The VerCors Verifier: A Progress Report",
booktitle="Computer Aided Verification",
year="2024",
publisher="Springer Nature Switzerland",
address="Cham",
pages="3--18",
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.",
isbn="978-3-031-65630-9",
doi="10.1007/978-3-031-65630-9_1"
}

{"_id":"EqEnB9prxF4RpSSSk","bibbaseid":"armborst-bos-vandenhaak-huisman-rubbens-akar-tasche-thevercorsverifieraprogressreport-2024","author_short":["Armborst, L.","Bos, P.","van den Haak, L. B.","Huisman, M.","Rubbens, R.","Şakar, Ö.","Tasche, P."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Armborst"],"firstnames":["Lukas"],"suffixes":[]},{"propositions":[],"lastnames":["Bos"],"firstnames":["Pieter"],"suffixes":[]},{"propositions":["van","den"],"lastnames":["Haak"],"firstnames":["Lars","B."],"suffixes":[]},{"propositions":[],"lastnames":["Huisman"],"firstnames":["Marieke"],"suffixes":[]},{"propositions":[],"lastnames":["Rubbens"],"firstnames":["Robert"],"suffixes":[]},{"propositions":[],"lastnames":["Şakar"],"firstnames":["Ömer"],"suffixes":[]},{"propositions":[],"lastnames":["Tasche"],"firstnames":["Philip"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Gurfinkel"],"firstnames":["Arie"],"suffixes":[]},{"propositions":[],"lastnames":["Ganesh"],"firstnames":["Vijay"],"suffixes":[]}],"title":"The VerCors Verifier: A Progress Report","booktitle":"Computer Aided Verification","year":"2024","publisher":"Springer Nature Switzerland","address":"Cham","pages":"3–18","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.","isbn":"978-3-031-65630-9","doi":"10.1007/978-3-031-65630-9_1","bibtex":"@InProceedings{Armborst24,\nauthor=\"Armborst, Lukas\nand Bos, Pieter\nand van den Haak, Lars B.\nand Huisman, Marieke\nand Rubbens, Robert\nand {\\c{S}}akar, {\\\"O}mer\nand Tasche, Philip\",\neditor=\"Gurfinkel, Arie\nand Ganesh, Vijay\",\ntitle=\"The VerCors Verifier: A Progress Report\",\nbooktitle=\"Computer Aided Verification\",\nyear=\"2024\",\npublisher=\"Springer Nature Switzerland\",\naddress=\"Cham\",\npages=\"3--18\",\nabstract=\"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.\",\nisbn=\"978-3-031-65630-9\",\ndoi=\"10.1007/978-3-031-65630-9_1\"\n}\n\n","author_short":["Armborst, L.","Bos, P.","van den Haak, L. B.","Huisman, M.","Rubbens, R.","Şakar, Ö.","Tasche, P."],"editor_short":["Gurfinkel, A.","Ganesh, V."],"key":"Armborst24","id":"Armborst24","bibbaseid":"armborst-bos-vandenhaak-huisman-rubbens-akar-tasche-thevercorsverifieraprogressreport-2024","role":"author","urls":{},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/utwente-fmt/vercors-web/master/static/references.bib","dataSources":["cCvCnPTRQYq3qPe9y"],"keywords":[],"search_terms":["vercors","verifier","progress","report","armborst","bos","van den haak","huisman","rubbens","şakar","tasche"],"title":"The VerCors Verifier: A Progress Report","year":2024}