Backward Refinement for Verifying Distributed Algorithms

K. Sere
Marina Waldén

In 6th NWPT, page 347

Abstract:

We present a new 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 correctness-preserving steps. At each step some mechanism of the algorithm is identified and abstracted away while the basic computation in the original algorithm is preserved. In this way the algorithm becomes more coarse-grained. Only the essential parts of the algorithm are then left for final verification.

Comments
Sere: University of Kuopio, Department of Computer Science and Applied Mathematics, P.O.Box 1627, SF-70211 Kuopio, Finland. Email: Kaisa.Sere@uku.fi. Waldén: Åbo Akademi University, Department of Computer Science, SF-20520 Turku, Finland. Email: mwalden@abo.fi.

Available as PostScript, DVI.

BRICS WWW home page