Safety and Liveness in Concurrent Pointer Programs

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

    7 Citations (Scopus)

    Abstract

    The incorrect use of pointers is one of the most common source of software errors. Concurrency has a similar characteristic. Proving the correctness of concurrent pointer manipulating programs, let alone algorithmically, is a highly non-trivial task. This paper proposes an automated verification technique for concurrent programs that manipulate linked lists. Key issues of our approach are: automata (with fairness constraints), heap abstractions that are tailored to the program and property to be checked, first-order temporal logic, and a tableau-based model-checking algorithm.
    Original languageUndefined
    Title of host publicationProceedings of the 4th Internatinal Symposium on Formal Methods for Components and Objects
    EditorsFrank S. de Boer, Marcello M. Bonsangue, Susanne Graf, Willem-Paul de Roever
    Place of PublicationBerlin
    PublisherSpringer
    Pages280-312
    Number of pages33
    ISBN (Print)978-3-540-36749-9
    DOIs
    Publication statusPublished - 2006

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Numbersuppl 2/4111
    Volume4111
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Keywords

    • EWI-8522
    • METIS-237770
    • IR-63805

    Cite this

    Distefano, D. S., Katoen, J. P., & Rensink, A. (2006). Safety and Liveness in Concurrent Pointer Programs. In F. S. de Boer, M. M. Bonsangue, S. Graf, & W-P. de Roever (Eds.), Proceedings of the 4th Internatinal Symposium on Formal Methods for Components and Objects (pp. 280-312). [10.1007/11804192_14] (Lecture Notes in Computer Science; Vol. 4111, No. suppl 2/4111). Berlin: Springer. https://doi.org/10.1007/11804192_14
    Distefano, D.S. ; Katoen, Joost P. ; Rensink, Arend. / Safety and Liveness in Concurrent Pointer Programs. Proceedings of the 4th Internatinal Symposium on Formal Methods for Components and Objects. editor / Frank S. de Boer ; Marcello M. Bonsangue ; Susanne Graf ; Willem-Paul de Roever. Berlin : Springer, 2006. pp. 280-312 (Lecture Notes in Computer Science; suppl 2/4111).
    @inproceedings{8fd64808d9c2412295a34c091a77228b,
    title = "Safety and Liveness in Concurrent Pointer Programs",
    abstract = "The incorrect use of pointers is one of the most common source of software errors. Concurrency has a similar characteristic. Proving the correctness of concurrent pointer manipulating programs, let alone algorithmically, is a highly non-trivial task. This paper proposes an automated verification technique for concurrent programs that manipulate linked lists. Key issues of our approach are: automata (with fairness constraints), heap abstractions that are tailored to the program and property to be checked, first-order temporal logic, and a tableau-based model-checking algorithm.",
    keywords = "EWI-8522, METIS-237770, IR-63805",
    author = "D.S. Distefano and Katoen, {Joost P.} and Arend Rensink",
    note = "Revised Lectures",
    year = "2006",
    doi = "10.1007/11804192_14",
    language = "Undefined",
    isbn = "978-3-540-36749-9",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    number = "suppl 2/4111",
    pages = "280--312",
    editor = "{de Boer}, {Frank S.} and Bonsangue, {Marcello M.} and Susanne Graf and {de Roever}, Willem-Paul",
    booktitle = "Proceedings of the 4th Internatinal Symposium on Formal Methods for Components and Objects",

    }

    Distefano, DS, Katoen, JP & Rensink, A 2006, Safety and Liveness in Concurrent Pointer Programs. in FS de Boer, MM Bonsangue, S Graf & W-P de Roever (eds), Proceedings of the 4th Internatinal Symposium on Formal Methods for Components and Objects., 10.1007/11804192_14, Lecture Notes in Computer Science, no. suppl 2/4111, vol. 4111, Springer, Berlin, pp. 280-312. https://doi.org/10.1007/11804192_14

    Safety and Liveness in Concurrent Pointer Programs. / Distefano, D.S.; Katoen, Joost P.; Rensink, Arend.

    Proceedings of the 4th Internatinal Symposium on Formal Methods for Components and Objects. ed. / Frank S. de Boer; Marcello M. Bonsangue; Susanne Graf; Willem-Paul de Roever. Berlin : Springer, 2006. p. 280-312 10.1007/11804192_14 (Lecture Notes in Computer Science; Vol. 4111, No. suppl 2/4111).

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

    TY - GEN

    T1 - Safety and Liveness in Concurrent Pointer Programs

    AU - Distefano, D.S.

    AU - Katoen, Joost P.

    AU - Rensink, Arend

    N1 - Revised Lectures

    PY - 2006

    Y1 - 2006

    N2 - The incorrect use of pointers is one of the most common source of software errors. Concurrency has a similar characteristic. Proving the correctness of concurrent pointer manipulating programs, let alone algorithmically, is a highly non-trivial task. This paper proposes an automated verification technique for concurrent programs that manipulate linked lists. Key issues of our approach are: automata (with fairness constraints), heap abstractions that are tailored to the program and property to be checked, first-order temporal logic, and a tableau-based model-checking algorithm.

    AB - The incorrect use of pointers is one of the most common source of software errors. Concurrency has a similar characteristic. Proving the correctness of concurrent pointer manipulating programs, let alone algorithmically, is a highly non-trivial task. This paper proposes an automated verification technique for concurrent programs that manipulate linked lists. Key issues of our approach are: automata (with fairness constraints), heap abstractions that are tailored to the program and property to be checked, first-order temporal logic, and a tableau-based model-checking algorithm.

    KW - EWI-8522

    KW - METIS-237770

    KW - IR-63805

    U2 - 10.1007/11804192_14

    DO - 10.1007/11804192_14

    M3 - Conference contribution

    SN - 978-3-540-36749-9

    T3 - Lecture Notes in Computer Science

    SP - 280

    EP - 312

    BT - Proceedings of the 4th Internatinal Symposium on Formal Methods for Components and Objects

    A2 - de Boer, Frank S.

    A2 - Bonsangue, Marcello M.

    A2 - Graf, Susanne

    A2 - de Roever, Willem-Paul

    PB - Springer

    CY - Berlin

    ER -

    Distefano DS, Katoen JP, Rensink A. Safety and Liveness in Concurrent Pointer Programs. In de Boer FS, Bonsangue MM, Graf S, de Roever W-P, editors, Proceedings of the 4th Internatinal Symposium on Formal Methods for Components and Objects. Berlin: Springer. 2006. p. 280-312. 10.1007/11804192_14. (Lecture Notes in Computer Science; suppl 2/4111). https://doi.org/10.1007/11804192_14