An Abstraction Technique for Describing Concurrent Program Behaviour

Wytse Oortwijn, Stefan Blom, Dilian Gurov, Marieke Huisman, M. Zaharieva

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

    9 Citations (Scopus)
    2 Downloads (Pure)

    Abstract

    This paper presents a technique to reason about functional properties of shared-memory concurrent software by means of abstraction. The abstract behaviour of the program is described using process algebras. In the program we indicate which concrete atomic steps correspond to the actions that are used in the process algebra term. Each action comes with a specification that describes its effect on the shared state. Program logics are used to show that the concrete program steps adhere to this specification. Separately, we also use program logics to prove that the program behaves as described by the process algebra term. Finally, via process algebraic reasoning we derive properties that hold for the program from its abstraction. This technique allows reasoning about the behaviour of highly concurrent, non-deterministic and possibly non-terminating programs. The paper discusses various verification examples to illustrate our approach. The verification technique is implemented as part of the VerCors toolset. We demonstrate that our technique is capable of verifying data- and control-flow properties that are hard to verify with alternative approaches, especially with mechanised tool support.
    Original languageEnglish
    Title of host publicationVerified Software. Theories, Tools, and Experiments
    Subtitle of host publication9th International Conference, VSTTE 2017, Heidelberg, Germany, July 22-23, 2017, Revised Selected Papers
    EditorsAndrei Paskevich, Thomas Wies
    PublisherSpringer
    Pages191-209
    Number of pages19
    ISBN (Electronic)978-3-319-72308-2
    ISBN (Print)978-3-319-72307-5
    DOIs
    Publication statusPublished - 2017
    Event9th Working Conference on Verified Software 2017: Theories, Tools, and Experiments - Heidelberg, Germany
    Duration: 22 Jul 201723 Jul 2017
    Conference number: 9
    https://vstte17.lri.fr/

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume10712

    Conference

    Conference9th Working Conference on Verified Software 2017
    Abbreviated titleVSTTE 2017
    CountryGermany
    CityHeidelberg
    Period22/07/1723/07/17
    OtherCo-located with the 29th International Conference on Computer-Aided Verification (CAV 2017)
    Internet address

    Fingerprint Dive into the research topics of 'An Abstraction Technique for Describing Concurrent Program Behaviour'. Together they form a unique fingerprint.

  • Cite this

    Oortwijn, W., Blom, S., Gurov, D., Huisman, M., & Zaharieva, M. (2017). An Abstraction Technique for Describing Concurrent Program Behaviour. In A. Paskevich, & T. Wies (Eds.), Verified Software. Theories, Tools, and Experiments: 9th International Conference, VSTTE 2017, Heidelberg, Germany, July 22-23, 2017, Revised Selected Papers (pp. 191-209). (Lecture Notes in Computer Science; Vol. 10712). Springer. https://doi.org/10.1007/978-3-319-72308-2_12