Using SPIN to model check concurrent algorithms, using a translation from C to Promela
Ke Jiang, Bengt Jönsson · KTH Publication Database DiVA (KTH Royal Institute of Technology) · 2009
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.