The VerCors Tool Set: Verification of Parallel and Concurrent Software

Stefan Blom; Saeed Darabi; Marieke Huisman; Wytse Oortwijn

doi:10.1007/978-3-319-66845-1_7

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 proceeding › Conference contribution › Academic › peer-review

28 Citations (Scopus)

6 Downloads (Pure)

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.

Original language	English
Title of host publication	Integrated Formal Methods
Subtitle of host publication	13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings
Editors	Nadia Polikarpova, Steve Schneider
Publisher	Springer
Pages	102-110
Number of pages	9
ISBN (Print)	978-3-319-66844-4
DOIs	https://doi.org/10.1007/978-3-319-66845-1_7
Publication status	Published - 2017
Event	13th International Conference on integrated Formal Methods 2017 - Cavallerizza Reale, Torino, Italy Duration: 18 Sep 2017 → 22 Sep 2017 Conference number: 13 http://ifm2017.di.unito.it/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	10510

Conference

Conference	13th International Conference on integrated Formal Methods 2017
Abbreviated title	IFM 2017
Country	Italy
City	Torino
Period	18/09/17 → 22/09/17
Internet address	http://ifm2017.di.unito.it/

Access to Document

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

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. https://doi.org/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",

address = "Netherlands",

note = "13th International Conference on integrated Formal Methods 2017, IFM 2017 ; Conference date: 18-09-2017 Through 22-09-2017",

url = "http://ifm2017.di.unito.it/",

}

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. https://doi.org/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 proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - The VerCors Tool Set

T2 - 13th International Conference on integrated Formal Methods 2017

AU - Blom, Stefan

AU - Darabi, Saeed

AU - Huisman, Marieke

AU - Oortwijn, Wytse

N1 - Conference code: 13

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

A2 - Polikarpova, Nadia

A2 - Schneider, Steve

PB - Springer

Y2 - 18 September 2017 through 22 September 2017

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). https://doi.org/10.1007/978-3-319-66845-1_7

The VerCors Tool Set: Verification of Parallel and Concurrent Software

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this