Using SPIN to model check concurrent algorithms, using a translation from C to Promela

This paper addresses the problem of automatically verifying correctness of concurrent algorithms, e.g., as found inconcurrent implementations of common data structures, using model checking. In order to use a model checker to analyze programs in, e.g., C, one must first translate programs to the input language of the model checker. Since our aim is to use SPIN, we present an automated translation from a subset of C to Promela. This translation is able to handle features not covered by previous such translations, notable pointer structures and function calls. We illustrate the application of our translation to a concurrent queue algorithm by Michael and Scott.automated verification of highly concurrent algorithmsUPMAR