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 proceedingConference contributionAcademicpeer-review

    28 Citations (Scopus)
    6 Downloads (Pure)


    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 languageEnglish
    Title of host publicationIntegrated Formal Methods
    Subtitle of host publication13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings
    EditorsNadia Polikarpova, Steve Schneider
    Number of pages9
    ISBN (Print)978-3-319-66844-4
    Publication statusPublished - 2017
    Event13th International Conference on integrated Formal Methods 2017 - Cavallerizza Reale, Torino, Italy
    Duration: 18 Sep 201722 Sep 2017
    Conference number: 13

    Publication series

    NameLecture Notes in Computer Science


    Conference13th International Conference on integrated Formal Methods 2017
    Abbreviated titleIFM 2017
    Internet address


    Dive into the research topics of 'The VerCors Tool Set: Verification of Parallel and Concurrent Software'. Together they form a unique fingerprint.

    Cite this