Verifying Functional Behaviour of Concurrent Programs

M. Zaharieva, Marieke Huisman, Stefan Blom

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

    1 Citation (Scopus)
    55 Downloads (Pure)

    Abstract

    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 (ACM)
    Pages4:1-4:6
    Number of pages6
    ISBN (Print)978-1-4503-2866-1
    DOIs
    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
    http://ecs.victoria.ac.nz/Events/FTfJP2014/

    Publication series

    Name
    PublisherACM

    Workshop

    Workshop16th Workshop on Formal Techniques for Java-like Programs, FTfJP 2014
    Abbreviated titleFTfJP
    CountrySweden
    CityUppsala
    Period28/07/1428/07/14
    Internet address

    Keywords

    • 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

    Zaharieva, M., Huisman, M., & Blom, S. (2014). Verifying Functional Behaviour of Concurrent Programs. In D. Pearce (Ed.), FTfJP'14: Proceedings of 16th Workshop on Formal Techniques for Java-like Programs (pp. 4:1-4:6). New York: Association for Computing Machinery (ACM). https://doi.org/10.1145/2635631.2635849
    Zaharieva, M. ; Huisman, Marieke ; Blom, Stefan. / Verifying Functional Behaviour of Concurrent Programs. FTfJP'14: Proceedings of 16th Workshop on Formal Techniques for Java-like Programs. editor / D. Pearce. New York : Association for Computing Machinery (ACM), 2014. pp. 4:1-4:6
    @inproceedings{c0081c376f294fa6956cb069c672f5f8,
    title = "Verifying Functional Behaviour of Concurrent Programs",
    abstract = "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.",
    keywords = "EWI-24914, CR-D.1.3, CR-D.2.4, concurrent programsmodular verificationbehavioural specifications, METIS-305947, Modular Verification, IR-91896, Concurrent programs, behavioural specifications",
    author = "M. Zaharieva and Marieke Huisman and Stefan Blom",
    note = "10.1145/2635631.2635849",
    year = "2014",
    month = "7",
    doi = "10.1145/2635631.2635849",
    language = "Undefined",
    isbn = "978-1-4503-2866-1",
    publisher = "Association for Computing Machinery (ACM)",
    pages = "4:1--4:6",
    editor = "D. Pearce",
    booktitle = "FTfJP'14: Proceedings of 16th Workshop on Formal Techniques for Java-like Programs",
    address = "United States",

    }

    Zaharieva, M, Huisman, M & Blom, S 2014, Verifying Functional Behaviour of Concurrent Programs. in D Pearce (ed.), FTfJP'14: Proceedings of 16th Workshop on Formal Techniques for Java-like Programs. Association for Computing Machinery (ACM), New York, pp. 4:1-4:6, 16th Workshop on Formal Techniques for Java-like Programs, FTfJP 2014, Uppsala, Sweden, 28/07/14. https://doi.org/10.1145/2635631.2635849

    Verifying Functional Behaviour of Concurrent Programs. / Zaharieva, M.; Huisman, Marieke; Blom, Stefan.

    FTfJP'14: Proceedings of 16th Workshop on Formal Techniques for Java-like Programs. ed. / D. Pearce. New York : Association for Computing Machinery (ACM), 2014. p. 4:1-4:6.

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

    TY - GEN

    T1 - Verifying Functional Behaviour of Concurrent Programs

    AU - Zaharieva, M.

    AU - Huisman, Marieke

    AU - Blom, Stefan

    N1 - 10.1145/2635631.2635849

    PY - 2014/7

    Y1 - 2014/7

    N2 - 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.

    AB - 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.

    KW - EWI-24914

    KW - CR-D.1.3

    KW - CR-D.2.4

    KW - concurrent programsmodular verificationbehavioural specifications

    KW - METIS-305947

    KW - Modular Verification

    KW - IR-91896

    KW - Concurrent programs

    KW - behavioural specifications

    U2 - 10.1145/2635631.2635849

    DO - 10.1145/2635631.2635849

    M3 - Conference contribution

    SN - 978-1-4503-2866-1

    SP - 4:1-4:6

    BT - FTfJP'14: Proceedings of 16th Workshop on Formal Techniques for Java-like Programs

    A2 - Pearce, D.

    PB - Association for Computing Machinery (ACM)

    CY - New York

    ER -

    Zaharieva M, Huisman M, Blom S. Verifying Functional Behaviour of Concurrent Programs. In Pearce D, editor, FTfJP'14: Proceedings of 16th Workshop on Formal Techniques for Java-like Programs. New York: Association for Computing Machinery (ACM). 2014. p. 4:1-4:6 https://doi.org/10.1145/2635631.2635849