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 条
  • [31] Solution of third-order Emden-Fowler-type equations using wavelet methods
    Khan, Arshad
    Faheem, Mo
    Raza, Akmal
    ENGINEERING COMPUTATIONS, 2021, 38 (06) : 2850 - 2881
  • [32] An algorithm to compute invariant sets for third-order switched systems
    Garcia-Gutierrez, J. B.
    Benitez-Trujillo, F.
    Perez, C.
    JOURNAL OF COMPUTATIONAL AND APPLIED MATHEMATICS, 2017, 318 : 348 - 353
  • [33] Optimal Feedback Arising in a Third-Order Dynamics with Boundary Controls and Infinite Horizon
    Irena Lasiecka
    Roberto Triggiani
    Journal of Optimization Theory and Applications, 2022, 193 : 831 - 855
  • [34] Optimal Feedback Arising in a Third-Order Dynamics with Boundary Controls and Infinite Horizon
    Lasiecka, Irena
    Triggiani, Roberto
    JOURNAL OF OPTIMIZATION THEORY AND APPLICATIONS, 2022, 193 (1-3) : 831 - 855
  • [35] A Consensus Algorithm Based on Partial Third-order Neighbors' Information
    Yan Z.-Q.
    Ge L.
    Zhang Y.-Y.
    Dou L.
    Zidonghua Xuebao/Acta Automatica Sinica, 2021, 47 (09): : 2285 - 2291
  • [36] EXPLICIT THIRD-ORDER ALGORITHM WITH COURANT NUMBER THREE.
    Forster, K.
    Zeitschrift fur angewandte Mathematik und Mechanik, 1988, 68 (05):
  • [37] Existence of Unbounded Solutions for a Third-Order Boundary Value Problem on Infinite Intervals
    Lian, Hairong
    Zhao, Junfang
    DISCRETE DYNAMICS IN NATURE AND SOCIETY, 2012, 2012
  • [38] A note on some new iterative methods with third-order convergence
    Wu, Qingbiao
    Ren, Hongmin
    APPLIED MATHEMATICS AND COMPUTATION, 2007, 188 (02) : 1790 - 1793
  • [39] Compact third-order limiter functions for finite volume methods
    Cada, Miroslav
    Torrilhon, Manuel
    JOURNAL OF COMPUTATIONAL PHYSICS, 2009, 228 (11) : 4118 - 4145
  • [40] A family of fifth-order iterations composed of Newton and third-order methods
    Kou, Jisheng
    Li, Yitian
    Wang, Xiuhua
    APPLIED MATHEMATICS AND COMPUTATION, 2007, 186 (02) : 1258 - 1262