Author(s): Steggles LJ
Abstract: We consider using third--order algebraic methods to specify and equationally verify an infinite systolic algorithm for convolution. The detailed case study we present provides an interesting insight into the use of third--order algebra as a formal framework for developing families of computing systems. We consider using purely equational reasoning in our verification proofs and in particular, using the rule of free variable induction. We conclude by considering how our verification proofs can be automated using rewriting techniques.
Keywords: formal verification, higher-order algebraic methods, infinite systolic algorithms, term rewriting