The VerCors Project: Setting Up Basecamp

A. Amighi, Stefan Blom, Marieke Huisman, M. Zaharieva

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

    13 Citations (Scopus)
    2 Downloads (Pure)


    This paper describes the first results and on-going work in the VerCors project. The VerCors project is about Verification of Concurrent Data Structures. Its goal is to develop a specification language and program logic for concurrent programs, and in particular for concurrent data structures, as these are the essential building blocks of many different concurrent programs. The program logic is based on our earlier work on permission-based separation logic for Java. This is an extension of Hoare logic that is particularly convenient to reason about concurrent programs. The paper first describes the tool set that is currently being built to support reasoning with this logic. It supports a specification language that combines features of separation logic with JML. For the verification, the program and its annotations are encoded into Chalice, and then we reuse the Chalice translation to Boogie to generate the proof obligations. Next, the paper describes our first results on data structure specifications. We use histories to keep track of the changes to the data structures, and we show how these histories allow us to derive other conclusions about the data structure implementations. We also discuss how we plan to reason about volatile variables, and how we will use this to verify lock-free data structures. Throughout the paper, we discuss our plans for future work within the VerCors project.
    Original languageUndefined
    Title of host publicationSixth Workshop Programming Languages meets Program Verification (PLPV 2012)
    Place of PublicationNew York
    PublisherAssociation for Computing Machinery
    Number of pages12
    ISBN (Print)978-1-4503-1125-0
    Publication statusPublished - 24 Jan 2012
    EventSixth Workshop Programming Languages meets Program Verification, PLPV 2012 - Philadelphia, PA, USA
    Duration: 24 Jan 201224 Jan 2012

    Publication series



    WorkshopSixth Workshop Programming Languages meets Program Verification, PLPV 2012
    Other24 January 2012


    • IR-79578
    • METIS-296421
    • Concurrency
    • Separation Logic
    • CR-F.3.1
    • EWI-21412
    • EC Grant Agreement nr.: FP7/258405
    • CR-D.2.4
    • Permissions

    Cite this