Safety and Liveness in Concurrent Pointer Programs

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

    8 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