Verification of mutual exclusion algorithms with SMV system

A mutual exclusion algorithm can exhibit intricate behavior for which correctness can be hard to establish. We demonstrate automatic verification of five algorithms by symbolic model checking. We used the SMV tool which enables property specification in computation tree logic and allows us to impose fairness constraints on a model. For each algorithm we verify safety, liveness, nonblocking and no strict ordering properties.