Verification of a systolic algorithm for string comparison
L. Kossen, W. P. Weijland · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1987
A self-timed systolic system computing the edit distance between two strings is proved correct by means of an algebraical concurrency theory ACP (Algebra of Communicating Processes, [BK1)).A systolic system is a system consisting of a great number of concurrently operating and cooperating elements.In the system described here (also discussed in [LL)), the flow of control is regulated by the elements themselves: the system is self-timed.A formal approach can be helpful to construct complex systems such as VLSI-circuits.Other verifications of systolic algorithms can be found in [KW] and [WE].