Verification of Concurrent Software with VerCors

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

Abstract

Concurrent software is inherently error-prone, due to the possible interactions and subtle interplays between the parallel computations. As a result, error prediction and tracing the sources of errors often is difficult. In particular, rerunning an execution with exactly the same input might not lead to the same error. To improve this situation, we need techniques that can provide static guarantees about the behaviour of a concurrent program. In this presentation, I present an approach based on program annotations, which is supported by the VerCors tool set. I will present the general set up of the approach, and discuss what kind of programs can be verified using this approach. Then I will dive into one concrete example, namely where we use the VerCors verification techniques to prove that compiler directives for program parallellisations (as done in OpenMP, for example) cannot change the behaviour of the program.
LanguageEnglish
Title of host publicationProceedings of the 29th Nordic Workshop on Programming Theory (NWPT)
EditorsMarina Walden
Pages2
Number of pages1
StatePublished - 2017
Event29th Nordic Workshop on Programming Theory 2017 - Turku, Finland
Duration: 1 Nov 20173 Nov 2017
Conference number: 29
https://research.it.abo.fi/nwpt17/

Publication series

NameTUCS lecture notes
No.27

Conference

Conference29th Nordic Workshop on Programming Theory 2017
Abbreviated titleNWPT 2017
CountryFinland
CityTurku
Period1/11/173/11/17
Internet address

Cite this

Huisman, M. (2017). Verification of Concurrent Software with VerCors. In M. Walden (Ed.), Proceedings of the 29th Nordic Workshop on Programming Theory (NWPT) (pp. 2). (TUCS lecture notes; No. 27).
Huisman, Marieke. / Verification of Concurrent Software with VerCors. Proceedings of the 29th Nordic Workshop on Programming Theory (NWPT). editor / Marina Walden. 2017. pp. 2 (TUCS lecture notes; 27).
@inproceedings{7fa020bf95bd4ca6a4f1aaed05c3bc18,
title = "Verification of Concurrent Software with VerCors",
abstract = "Concurrent software is inherently error-prone, due to the possible interactions and subtle interplays between the parallel computations. As a result, error prediction and tracing the sources of errors often is difficult. In particular, rerunning an execution with exactly the same input might not lead to the same error. To improve this situation, we need techniques that can provide static guarantees about the behaviour of a concurrent program. In this presentation, I present an approach based on program annotations, which is supported by the VerCors tool set. I will present the general set up of the approach, and discuss what kind of programs can be verified using this approach. Then I will dive into one concrete example, namely where we use the VerCors verification techniques to prove that compiler directives for program parallellisations (as done in OpenMP, for example) cannot change the behaviour of the program.",
author = "Marieke Huisman",
year = "2017",
language = "English",
isbn = "978-952-12-3608-2",
series = "TUCS lecture notes",
number = "27",
pages = "2",
editor = "Marina Walden",
booktitle = "Proceedings of the 29th Nordic Workshop on Programming Theory (NWPT)",

}

Huisman, M 2017, Verification of Concurrent Software with VerCors. in M Walden (ed.), Proceedings of the 29th Nordic Workshop on Programming Theory (NWPT). TUCS lecture notes, no. 27, pp. 2, 29th Nordic Workshop on Programming Theory 2017, Turku, Finland, 1/11/17.

Verification of Concurrent Software with VerCors. / Huisman, Marieke.

Proceedings of the 29th Nordic Workshop on Programming Theory (NWPT). ed. / Marina Walden. 2017. p. 2 (TUCS lecture notes; No. 27).

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

TY - GEN

T1 - Verification of Concurrent Software with VerCors

AU - Huisman,Marieke

PY - 2017

Y1 - 2017

N2 - Concurrent software is inherently error-prone, due to the possible interactions and subtle interplays between the parallel computations. As a result, error prediction and tracing the sources of errors often is difficult. In particular, rerunning an execution with exactly the same input might not lead to the same error. To improve this situation, we need techniques that can provide static guarantees about the behaviour of a concurrent program. In this presentation, I present an approach based on program annotations, which is supported by the VerCors tool set. I will present the general set up of the approach, and discuss what kind of programs can be verified using this approach. Then I will dive into one concrete example, namely where we use the VerCors verification techniques to prove that compiler directives for program parallellisations (as done in OpenMP, for example) cannot change the behaviour of the program.

AB - Concurrent software is inherently error-prone, due to the possible interactions and subtle interplays between the parallel computations. As a result, error prediction and tracing the sources of errors often is difficult. In particular, rerunning an execution with exactly the same input might not lead to the same error. To improve this situation, we need techniques that can provide static guarantees about the behaviour of a concurrent program. In this presentation, I present an approach based on program annotations, which is supported by the VerCors tool set. I will present the general set up of the approach, and discuss what kind of programs can be verified using this approach. Then I will dive into one concrete example, namely where we use the VerCors verification techniques to prove that compiler directives for program parallellisations (as done in OpenMP, for example) cannot change the behaviour of the program.

M3 - Conference contribution

SN - 978-952-12-3608-2

T3 - TUCS lecture notes

SP - 2

BT - Proceedings of the 29th Nordic Workshop on Programming Theory (NWPT)

ER -

Huisman M. Verification of Concurrent Software with VerCors. In Walden M, editor, Proceedings of the 29th Nordic Workshop on Programming Theory (NWPT). 2017. p. 2. (TUCS lecture notes; 27).