[Wishnu Prasetya Home]

This is my orginal Ph.D. work. It contains the formalization and verification of the logic UNITY in the theorem prover HOL.

It actually features many more than just UNITY:

1. A theory of self-stabilization and convergence.
2. A theory of progress composition. More powerful than the classical UNITY.
   [Replaced by v1999 version]
3. A formalization of Lentfert's theorem for reducing a distributed self-stabilization algorithm to a much more abstract problem of round-solvability
4. A generalization of the above Lentfert's round solvability reduction to self-stabilization problems on hierarchical networks.

Code Download:

Download my v1995 UNITY libraries. Requires HOL 1988 (now archaic!).

1. I.S. W. B. Prasetya. Formalizing UNITY with HOL. Tech. Report UU-CS-1996-01.

2. I.S. W. B. Prasetya. Formal design of self-stabilizing programs. Tech. Report UU-CS-1995-07.

3. I.S.W.B. Prasetya, Mechanically Supported Design of Self-stabilizing Algorithms. Ph.D. thesis, Utrecht University 1995.