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

    25 Citations (Scopus)
    5 Downloads (Pure)

    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 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
    PublisherSpringer
    Pages102-110
    Number of pages9
    ISBN (Print)978-3-319-66844-4
    DOIs
    Publication statusPublished - 2017
    Event13th International Conference on integrated Formal Methods 2017 - Cavallerizza Reale, Torino, Italy
    Duration: 18 Sep 201722 Sep 2017
    Conference number: 13
    http://ifm2017.di.unito.it/

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume10510

    Conference

    Conference13th International Conference on integrated Formal Methods 2017
    Abbreviated titleIFM 2017
    CountryItaly
    CityTorino
    Period18/09/1722/09/17
    Internet address

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

    Cite this