Formal verification of Dijkstra's Self Stabilizing algorithm for ring networks.

Using NuSMV's powerful Linear Temporal Logic, we verify the safety, liveness and stabilization conditions on four distrubuted processes (both synchronus and asynchronus).