Verification of Concurrent Software with VerCors

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

    88 Downloads (Pure)

    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.
    Original languageEnglish
    Title of host publicationProceedings of the 29th Nordic Workshop on Programming Theory (NWPT)
    EditorsMarina Walden
    Pages2
    Number of pages1
    Publication statusPublished - 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
    Number27

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