Correctness proofs for systolic algorithms: a palindrome recognizer
W. P. Weijland · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1987
In designing VLSI-circuits it is very useful, if not necessary, to construct the specific circuit by placing simple components in regular configurations.Systolic systems are circuits built up from arrays of cells and therefore very suitable for formal analysis and induction methods.In case of a palindrome recognizer a correctness proof is given using bisimulation semantics with asynchronous cooperation.The proof is carried out in the formal setting of the Algebra of Communicating Processes (see [BK1]), which provides us with an algebraical theory and a convenient proof system.An extensive introduction to this theory is included in this paper.The palindrome recognizer has also been studied by Hennessy [HEN] in a setting of failure semantics with synchronous cooperation.