The VerCors Tool for Verification of Concurrent Programs

Stefan Blom, Marieke Huisman

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

    24 Citations (Scopus)
    125 Downloads (Pure)

    Abstract

    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
    PublisherSpringer
    Pages127-131
    Number of pages5
    ISBN (Print)978-3-319-06409-3
    DOIs
    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
    Volume8442
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference19th International Symposium on Formal Methods
    Abbreviated titleFM 2014
    CountrySingapore
    CitySingapore
    Period12/05/1416/05/14

    Keywords

    • 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

    Blom, S., & Huisman, M. (2014). The VerCors Tool for Verification of Concurrent Programs. In C. Jones, P. Pihlajasaari, & J. Sun (Eds.), Proceedings of the 19th International Symposium on Formal Methods, FM 2014 (pp. 127-131). (Lecture Notes in Computer Science; Vol. 8442). Berlin: Springer. https://doi.org/10.1007/978-3-319-06410-9_9