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