VerCors: A Layered Approach to Practical Verification of Concurrent Software

A. Amighi, Stefan Blom, Marieke Huisman

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

    10 Citations (Scopus)
    147 Downloads (Pure)

    Abstract

    This paper discusses how several concurrent program verification techniques can be combined in a layered approach, where each layer is especially suited to verify one aspect of concurrent programs, thus making verification of concurrent programs practical. At the bottom layer, we use a combination of implicit dynamic frames and CSL-style resource invariants, to reason about data race freedom of programs. We illustrate this on the verification of a lock-free queue implementation. On top of this, layer 2 enables reasoning about resource invariants that express a relationship between thread-local and shared variables. This is illustrated by the verification of a reentrant lock implementation, where thread-locality is used to specify for a thread which locks it holds, while there is a global notion of ownership, expressing for a lock by which thread it is held. Finally, the top layer adds a notion of histories to reason about functional properties. We illustrate how this is used to prove that the lock-free queue preserves the order of elements, without having to reverify the aspects related to data race freedom.
    Original languageUndefined
    Title of host publicationProceedings of the 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP 2016)
    Place of PublicationUSA
    PublisherIEEE
    Pages495-503
    Number of pages9
    ISBN (Print)978-1-4673-8775-0
    DOIs
    Publication statusPublished - Feb 2016
    Event24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2016 - Heraklion, Crete, Greece
    Duration: 17 Feb 201619 Feb 2016
    Conference number: 24

    Publication series

    Name
    PublisherIEEE Computer Society
    ISSN (Print)2377-5750

    Conference

    Conference24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2016
    Abbreviated titlePDP
    Country/TerritoryGreece
    CityHeraklion, Crete,
    Period17/02/1619/02/16

    Keywords

    • EWI-27395
    • Program Verification
    • METIS-320885
    • IR-102859
    • Separation Logic

    Cite this