ePrints

Verifying an infinite systolic algorithm using third-order equational methods

Lookup NU author(s): Dr Jason Steggles

Downloads

Full text for this publication is not currently held within this repository. Alternative links are provided below where available.

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. © 2005 Elsevier Inc. All rights reserved.

Publication metadata

Author(s): Steggles LJ

Publication type: Article

Publication status: Published

Journal: Journal of Logic and Algebraic Programming

Year: 2006

Volume: 69

Issue: 1-2

Pages: 75-92

ISSN (print): 1567-8326

ISSN (electronic): 1873-5940

Publisher: Elsevier BV

URL: http://dx.doi.org/10.1016/j.jlap.2005.10.006

DOI: 10.1016/j.jlap.2005.10.006

Altmetrics

Share