The VerCors Tool for Verification of Concurrent Programs

Stefan Blom, Marieke Huisman

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    40 Citations (Scopus)
    421 Downloads (Pure)


    The VerCors tool implements thread-modular static verification of concurrent programs, annotated with functional properties and heap access permissions. The tool supports both generic multithreaded and vector-based programming models. In particular, it can verify multithreaded programs written in Java, specified with JML extended with separation logic. It can also verify parallelizable programs written in a toy language that supports the characteristic features of OpenCL. The tool verifies programs by first encoding the specified program into a much simpler programming language and then applying the Chalice verifier to the simplified program. In this paper we discuss both the implementation of the tool and the features of its specification language.
    Original languageUndefined
    Title of host publicationProceedings of the 19th International Symposium on Formal Methods, FM 2014
    EditorsCliff Jones, Pekka Pihlajasaari, Jun Sun
    Place of PublicationBerlin
    Number of pages5
    ISBN (Print)978-3-319-06409-3
    Publication statusPublished - May 2014
    Event19th International Symposium on Formal Methods - Singapore, Singapore
    Duration: 12 May 201416 May 2014
    Conference number: 19th

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    Conference19th International Symposium on Formal Methods
    Abbreviated titleFM 2014


    • EC Grant Agreement nr.: FP7/2007-2013
    • EC Grant Agreement nr.: FP7/258405
    • EC Grant Agreement nr.: FP7/287767
    • METIS-309765
    • Separation Logic
    • Verification Tools
    • IR-94062
    • EWI-25487

    Cite this