Verifying class invariants in concurrent programs

M. Zaharieva, Marieke Huisman

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

    124 Downloads (Pure)


    Class invariants are a highly useful feature for the verification of object-oriented programs, because they can be used to capture all valid object states. In a sequential program setting, the validity of class invariants is typically described in terms of a visible state semantics, i.e., invariants only have to hold whenever a method begins or ends execution, and they may be broken inside a method body. However, in a concurrent setting, this restriction is no longer usable, because due to thread interleavings, any program state is potentially a visible state. In this paper we present a new approach for reasoning about class invariants in multithreaded programs. We allow a thread to explicitly break an invariant at specific program locations, while ensuring that no other thread can observe the broken invariant. We develop our technique in a permission-based separation logic environment. However, we deviate from separation logic's standard rules and allow a class invariant to express properties over shared memory locations (the invariant footprint), independently of the permissions on these locations. In this way, a thread may break or reestablish an invariant without holding permissions to all locations in its footprint. To enable modular verification, we adopt the restrictions of Muller's ownership-based type system.
    Original languageUndefined
    Title of host publicationProceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE 2014)
    EditorsStefania Gnesi, Arend Rensink
    Place of PublicationBerlin
    Number of pages16
    ISBN (Print)978-3-642-54803-1
    Publication statusPublished - Apr 2014
    Event17th International Conference on Fundamental Approaches to Software Engineering, FASE 2014 - Grenoble, France
    Duration: 5 Apr 201413 Apr 2014
    Conference number: 17

    Publication series

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


    Conference17th International Conference on Fundamental Approaches to Software Engineering, FASE 2014
    Abbreviated titleFASE


    • EWI-24902
    • CR-D.2.4
    • Program Verification
    • METIS-305941
    • IR-91765
    • Class Invariants
    • Concurrency
    • Separation Logic

    Cite this