Verifying an infinite systolic algorithm using third-order equational methods

被引:1
|
作者
Steggles, L. J. [1 ]
机构
[1] Univ Newcastle, Sch Comp Sci, Newcastle Upon Tyne NE1 74U, Tyne & Wear, England
来源
JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING | 2006年 / 69卷 / 1-2期
关键词
higher-order algebra; third-order equational techniques; infinite systolic algorithm;
D O I
10.1016/j.jlap.2005.10.006
中图分类号
学科分类号
摘要
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. (C) 2005 Elsevier Inc. All rights reserved.
引用
收藏
页码:75 / 92
页数:18
相关论文
共 50 条
  • [1] Iterative Algorithm using Decoupling Method for third-order Tensor Deblurring
    EL Qate, Karima
    Mohaoui, Souad
    Hakim, Abdelilah
    Raghay, Said
    ANNALS OF THE UNIVERSITY OF CRAIOVA-MATHEMATICS AND COMPUTER SCIENCE SERIES, 2024, 51 (01): : 150 - 166
  • [2] Realization of algorithm for the computation of third-order cross moments using FPGA
    Qasim, Syed Manzoor
    Alshebeili, Saleh A.
    Khan, Ateeq A.
    Abbasi, Shuja A.
    2007 9TH INTERNATIONAL SYMPOSIUM ON SIGNAL PROCESSING AND ITS APPLICATIONS, VOLS 1-3, 2007, : 160 - 163
  • [3] Continuous Twisting Algorithm for Third-Order Systems
    Mendoza-Avila, Jesus
    Moreno, Jaime A.
    Fridman, Leonid M.
    IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2020, 65 (07) : 2814 - 2825
  • [5] Third-order family of methods in Banach spaces
    Chun, Changbum
    Stanica, Pantelimon
    Neta, Beny
    COMPUTERS & MATHEMATICS WITH APPLICATIONS, 2011, 61 (06) : 1665 - 1675
  • [6] Third-order iterative methods without using any Frechet derivative
    Amat, S
    Busquier, S
    Candela, V
    JOURNAL OF COMPUTATIONAL AND APPLIED MATHEMATICS, 2003, 158 (01) : 11 - 18
  • [8] CONTROLLABILITY OF NONLINEAR THIRD-ORDER DISPERSION INCLUSIONS WITH INFINITE DELAY
    Li, Meili
    Wang, Xiaoxia
    Wang, Haiqing
    ELECTRONIC JOURNAL OF DIFFERENTIAL EQUATIONS, 2013,
  • [9] High-speed systolic array for computing third-order cumulants
    Al-Turaigi, M.A.
    Alshebeili, S.A.
    Canadian Journal of Electrical and Computer Engineering, 1997, 22 (01): : 19 - 23
  • [10] A high-speed systolic array for computing third-order cumulants
    AlTuraigi, MA
    Alshebeili, SA
    CANADIAN JOURNAL OF ELECTRICAL AND COMPUTER ENGINEERING-REVUE CANADIENNE DE GENIE ELECTRIQUE ET INFORMATIQUE, 1997, 22 (01): : 19 - 23