Verification of concurrent systems with VerCors

Afshin Amighi, Stefan Blom, Saeed Darabi, Marieke Huisman, Wojciech Mostowski, Marina Zaharieva-Stojanovski

    Research output: Chapter in Book/Report/Conference proceedingChapterAcademic

    7 Citations (Scopus)
    16 Downloads (Pure)

    Abstract

    This paper presents the VerCors approach to verification of concurrent software. It first discusses why verification of concurrent software is important, but also challenging. Then it shows how within the VerCors project we use permission-based separation logic to reason about multithreaded Java programs. We discuss in particular how we use the logic to use different implementations of synchronisers in verification, and how we reason about class invariance properties in a concurrent setting. Further, we also show how the approach is suited to reason about programs using a different concurrency paradigm, namely kernel programs using the Single Instruction Multiple Data paradigm. Concretely, we illustrate how permission-based separation logic is suitable to verify functional correctness properties of OpenCL kernels. All verification techniques discussed in this paper are supported by the VerCors tool set.
    Original languageEnglish
    Title of host publicationFormal Methods for Executable Software Models
    Subtitle of host publication14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems
    EditorsMarco Bernardo, Ferruccio Damiani, Reiner Hähnle, Einar Broch Johnsen, Ina Schaefer
    Place of PublicationCham
    PublisherSpringer
    Pages172-216
    Number of pages45
    ISBN (Electronic)978-3-319-07317-0
    ISBN (Print)978-3-319-07316-3
    DOIs
    Publication statusPublished - Jun 2014
    Event14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2014 - Bertinoro, Italy
    Duration: 16 Jun 201420 Jun 2014
    Conference number: 14

    Publication series

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

    Conference

    Conference14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2014
    Abbreviated titleSFM
    CountryItaly
    CityBertinoro
    Period16/06/1420/06/14

      Fingerprint

    Keywords

    • EC Grant Agreement nr.: FP7/287767
    • EC Grant Agreement nr.: FP7/2007-2013
    • EC Grant Agreement nr.: FP7/258405
    • CR-D.2.4
    • Global memory
    • Software verification
    • VerCors tool
    • Concurrency
    • Concurrent program
    • Concurrent system
    • Java modeling language
    • Class invariants

    Cite this

    Amighi, A., Blom, S., Darabi, S., Huisman, M., Mostowski, W., & Zaharieva-Stojanovski, M. (2014). Verification of concurrent systems with VerCors. In M. Bernardo, F. Damiani, R. Hähnle, E. Broch Johnsen, & I. Schaefer (Eds.), Formal Methods for Executable Software Models: 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (pp. 172-216). (Lecture Notes in Computer Science; Vol. 8483). Cham: Springer. https://doi.org/10.1007/978-3-319-07317-0_5