Verifying Functional Behaviour of Concurrent Programs

M. Zaharieva, Marieke Huisman, Stefan Blom

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

    2 Citations (Scopus)
    175 Downloads (Pure)


    Specifying the functional behaviour of a concurrent program can often be quite troublesome: it is hard to provide a stable method contract that can not be invalidated by other threads. In this paper we propose a novel modular technique for specifying and verifying behavioural properties in concurrent programs. Our approach uses history-based specifications. A history is a process algebra term built of actions, where each action represents an update over a heap location. Instead of describing the object's precise state, a method contract may describe the method's behaviour in terms of actions recorded in the history. The client class can later use the history to reason about the concrete state of the object. Our approach allows providing simple and intuitive specifications, while the logic is a simple extension of permission-based separation logic.
    Original languageUndefined
    Title of host publicationFTfJP'14: Proceedings of 16th Workshop on Formal Techniques for Java-like Programs
    EditorsD. Pearce
    Place of PublicationNew York
    PublisherAssociation for Computing Machinery
    Number of pages6
    ISBN (Print)978-1-4503-2866-1
    Publication statusPublished - Jul 2014
    Event16th Workshop on Formal Techniques for Java-like Programs, FTfJP 2014 - Uppsala, Sweden
    Duration: 28 Jul 201428 Jul 2014
    Conference number: 16

    Publication series



    Workshop16th Workshop on Formal Techniques for Java-like Programs, FTfJP 2014
    Abbreviated titleFTfJP
    Internet address


    • EWI-24914
    • CR-D.1.3
    • CR-D.2.4
    • concurrent programsmodular verificationbehavioural specifications
    • METIS-305947
    • Modular Verification
    • IR-91896
    • Concurrent programs
    • behavioural specifications

    Cite this