The following technical report is available from http://aib.informatik.rwth-aachen.de:
Verifying Concurrent List-Manipulating Programs by LTL Model Checking Joost-Pieter Katoen, Thomas Noll, and Stefan Rieger AIB 2007-06
We present a novel approach to the verification of concurrent pointer-manipulating programs which operate on singly-linked lists. By abstracting from chains (i.e., non-interrupted sublists) in the heap, we obtain a finite-state representation of all possible executions of a given program. The combination of a simple pointer logic for expressing heap properties and of temporal operators then allows us to employ standard LTL model checking techniques. The usability of this approach is demonstrated by establishing correctness properties of a producer/consumer system and of a concurrent garbage collector.