A Distributed Path Algorithm and Its Correctness Proof
David D. Wright, Fred B. Schneider · 1983
A distributed program is developed to allow a process in a network to determine a path from itself to any other process, assuming that the topology of the entire network is not known to any process and that each process knows only the names of the processes to which it is directly connected. The solution, written in CSP, is proved correct and deadlock-free.