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
    Event4th Internatinal Symposium on Formal Methods for Components and Objects, FMCO 2005 - Amsterdam, The Netherlands
    Duration: 1 Nov 20054 Nov 2005

    Publication series

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

    Conference

    Conference4th Internatinal Symposium on Formal Methods for Components and Objects, FMCO 2005
    Period1/11/054/11/05
    OtherNovember 1-4, 2005

    Keywords

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

    Cite this