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