Mechanical certification of systolic algorithms
type: Item
instance of: scholarly article
title: Mechanical certification of systolic algorithms
zbMATH Open document ID: 0677.68009
DOI: 10.1007/BF00245022
author: P. A. Subrahmanyam
author: Sudarshan P. Purushothaman
published in: Journal of Automated Reasoning
publication date: 1989-01-01T00:00:00Z
review text: The common practice in designing systolic algorithms is to finish with a description of interconnection network, flows of data and behaviour of every processing element. The proof of the correctness of the result is usually omitted. The problem of proving correctness of algorithms amounts to proving that the correct data arrives at the correct place at the correct time so as to produce the expected result. The paper reviewed presents one possible approach to accomplish it using Boyer-Moore theorem power (see \textit{R. S. Boyer} and \textit{J. S. Moore} [A computational logic (Academic Press, New York) (1979; Zbl 0448.68020)]). Particularly, the authors propose the methodology involving the following steps i) uncover recurrence equations from presentations (i.e. from functions that define the functionality of the processing elements and the communication paths), ii) solve the recurrence equations using input schedules as initial conditions to obtain a closed form solution (i.e. to find the values on all the input ports and accumulators in terms of the data fed from the external world), iii) prove that the array meets the output schedule from the closed form solution and they show how to carry out the second and the third steps using Boyer-Moore theorem prover. The whole process is explained in details by proving correctness of a systolic algorithm for a dynamic programming problem.
reviewed by: Jozef Vyskoč
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 4110073
zbMATH Keywords: systolic algorithms
zbMATH Keywords: program verification
zbMATH Keywords: theorem power
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1007/bf00245022
OpenAlex ID: W2026452251
Recommended article: Q3753931
Recommended article: Automatic verification of a class of systolic circuits
Recommended article: Q5699568
Recommended article: Q3792219
Recommended article: Q3761701
Recommended article: Synthesis of a new systolic architecture for the algebraic path problem
Recommended article: A verification system for concurrent programs based on the Boyer-Moore prover
Recommended article: Q4028129
Recommended article: Automated proofs of object code for a widely used microprocessor
description: scientific article; zbMATH DE number 4110073