Nordic Journal of Computing Bibliography

Kaisa Sere and Marina Waldén. Structuring and Verifying Distributed Algorithms. Nordic Journal of Computing, 8(2):193-218, Summer 2001.

We present a structuring and verification method for distributed algorithms. The basic idea is that an algorithm to be verified is stepwise transformed into a high level specification through a number of steps, so-called coarsenings. At each step some mechanism of the algorithm is identified, verified and removed while the basic computation of the original algorithm is preserved. The method is based on a program development technique called superposition and it is formalized within the refinement calculus. We will show the usefulness of the method by verifying a complex distributed algorithm for minimum-hop route maintenance due to Chu.

Categories and Subject Descriptors: D.2.4 [Software Engineering]: Program Verification; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs

Additional Key Words and Phrases: verifying programs, understanding programs, distributed systems, superposition refinement, action systems

Selected references


  • Nordic Journal of Computing homepage
  • Bibliography top level
  • Nordic Journal of Computing Author Index
  • Search the HBP database