The VerCors Tool Set: Verification of Parallel and Concurrent Software

Stefan Blom, Saeed Darabi, Marieke Huisman, Wytse Oortwijn

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2 Citations

Abstract

This paper reports on the VerCors tool set for verifying parallel and concurrent software. Its main characteristics are (i) that it can verify programs under different concurrency models, written in high-level programming languages, such as for example in Java, OpenCL and OpenMP; and (ii) that it can reason not only about race freedom and memory safety, but also about functional correctness. VerCors builds on top of existing verification technology, notably the Viper framework, by transforming the verification problem of programs written in a high-level programming language into a verification problem in the intermediate language of Viper. This paper presents three examples that illustrate how VerCors support verifying functional correctness of three different concurrency features: heterogeneous concurrency, kernels using barriers and atomic operations, and compiler directives for parallelisation.
LanguageEnglish
Title of host publicationIntegrated Formal Methods
Subtitle of host publication13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings
EditorsNadia Polikarpova, Steve Schneider
PublisherSpringer
Pages102-110
Number of pages9
ISBN (Print)978-3-319-66844-4
DOIs
StatePublished - 2017
Event13th International Conference on integrated Formal Methods 2017 - Cavallerizza Reale, Torino, Italy
Duration: 18 Sep 201722 Sep 2017
Conference number: 13
http://ifm2017.di.unito.it/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume10510

Conference

Conference13th International Conference on integrated Formal Methods 2017
Abbreviated titleIFM 2017
CountryItaly
CityTorino
Period18/09/1722/09/17
Internet address

Fingerprint

Computer programming languages
Data storage equipment

Cite this

Blom, S., Darabi, S., Huisman, M., & Oortwijn, W. (2017). The VerCors Tool Set: Verification of Parallel and Concurrent Software. In N. Polikarpova, & S. Schneider (Eds.), Integrated Formal Methods: 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings (pp. 102-110). (Lecture Notes in Computer Science; Vol. 10510). Springer. DOI: 10.1007/978-3-319-66845-1_7
Blom, Stefan ; Darabi, Saeed ; Huisman, Marieke ; Oortwijn, Wytse. / The VerCors Tool Set : Verification of Parallel and Concurrent Software. Integrated Formal Methods: 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings. editor / Nadia Polikarpova ; Steve Schneider. Springer, 2017. pp. 102-110 (Lecture Notes in Computer Science).
@inproceedings{11861b573b204938895bcc26805d90e4,
title = "The VerCors Tool Set: Verification of Parallel and Concurrent Software",
abstract = "This paper reports on the VerCors tool set for verifying parallel and concurrent software. Its main characteristics are (i) that it can verify programs under different concurrency models, written in high-level programming languages, such as for example in Java, OpenCL and OpenMP; and (ii) that it can reason not only about race freedom and memory safety, but also about functional correctness. VerCors builds on top of existing verification technology, notably the Viper framework, by transforming the verification problem of programs written in a high-level programming language into a verification problem in the intermediate language of Viper. This paper presents three examples that illustrate how VerCors support verifying functional correctness of three different concurrency features: heterogeneous concurrency, kernels using barriers and atomic operations, and compiler directives for parallelisation.",
author = "Stefan Blom and Saeed Darabi and Marieke Huisman and Wytse Oortwijn",
year = "2017",
doi = "10.1007/978-3-319-66845-1_7",
language = "English",
isbn = "978-3-319-66844-4",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "102--110",
editor = "Nadia Polikarpova and Steve Schneider",
booktitle = "Integrated Formal Methods",

}

Blom, S, Darabi, S, Huisman, M & Oortwijn, W 2017, The VerCors Tool Set: Verification of Parallel and Concurrent Software. in N Polikarpova & S Schneider (eds), Integrated Formal Methods: 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10510, Springer, pp. 102-110, 13th International Conference on integrated Formal Methods 2017, Torino, Italy, 18/09/17. DOI: 10.1007/978-3-319-66845-1_7

The VerCors Tool Set : Verification of Parallel and Concurrent Software. / Blom, Stefan; Darabi, Saeed; Huisman, Marieke; Oortwijn, Wytse.

Integrated Formal Methods: 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings. ed. / Nadia Polikarpova; Steve Schneider. Springer, 2017. p. 102-110 (Lecture Notes in Computer Science; Vol. 10510).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - The VerCors Tool Set

T2 - Verification of Parallel and Concurrent Software

AU - Blom,Stefan

AU - Darabi,Saeed

AU - Huisman,Marieke

AU - Oortwijn,Wytse

PY - 2017

Y1 - 2017

N2 - This paper reports on the VerCors tool set for verifying parallel and concurrent software. Its main characteristics are (i) that it can verify programs under different concurrency models, written in high-level programming languages, such as for example in Java, OpenCL and OpenMP; and (ii) that it can reason not only about race freedom and memory safety, but also about functional correctness. VerCors builds on top of existing verification technology, notably the Viper framework, by transforming the verification problem of programs written in a high-level programming language into a verification problem in the intermediate language of Viper. This paper presents three examples that illustrate how VerCors support verifying functional correctness of three different concurrency features: heterogeneous concurrency, kernels using barriers and atomic operations, and compiler directives for parallelisation.

AB - This paper reports on the VerCors tool set for verifying parallel and concurrent software. Its main characteristics are (i) that it can verify programs under different concurrency models, written in high-level programming languages, such as for example in Java, OpenCL and OpenMP; and (ii) that it can reason not only about race freedom and memory safety, but also about functional correctness. VerCors builds on top of existing verification technology, notably the Viper framework, by transforming the verification problem of programs written in a high-level programming language into a verification problem in the intermediate language of Viper. This paper presents three examples that illustrate how VerCors support verifying functional correctness of three different concurrency features: heterogeneous concurrency, kernels using barriers and atomic operations, and compiler directives for parallelisation.

U2 - 10.1007/978-3-319-66845-1_7

DO - 10.1007/978-3-319-66845-1_7

M3 - Conference contribution

SN - 978-3-319-66844-4

T3 - Lecture Notes in Computer Science

SP - 102

EP - 110

BT - Integrated Formal Methods

PB - Springer

ER -

Blom S, Darabi S, Huisman M, Oortwijn W. The VerCors Tool Set: Verification of Parallel and Concurrent Software. In Polikarpova N, Schneider S, editors, Integrated Formal Methods: 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings. Springer. 2017. p. 102-110. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-66845-1_7