Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
431231 | The Journal of Logic and Algebraic Programming | 2006 | 18 Pages |
Abstract
We consider using third-order equational methods to formally verify that an infinite systolic algorithm correctly implements a family of convolution functions. The detailed case study we present illustrates the use of third-order algebra as a formal framework for developing families of computing systems. It also provides an interesting insight into the use of infinite algorithms as a means of verifying a family of finite algorithms. 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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics