Verifying an Infinite Systolic Algorithm using Third-Order Algebraic Methods (2003)

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.

      • Date: 2003
      • Series Title: School of Computing Science Technical Report Series
      • Pages: 15
      • Institution: School of Computing Science, University of Newcastle upon Tyne
      • Publication type: Report
      • Bibliographic status: Published

      Keywords: formal verification, higher-order algebraic methods, infinite systolic algorithms, term rewriting

      Staff

      Dr Jason Steggles
      Senior Lecturer