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.
|Name||Lecture Notes in Computer Science|
|Conference||4th Internatinal Symposium on Formal Methods for Components and Objects, FMCO 2005|
|Period||1/11/05 → 4/11/05|
|Other||November 1-4, 2005|