Abstract
| 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 | |
| State | 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 |
Fingerprint
Cite this
}
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
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 -