Verifying an infinite systolic algorithm using third-order equational methods

DOI10.1016/J.JLAP.2005.10.006MaRDI QIDQ2500698zbMATHOpenAlexFDO

Authors L. J. Steggles

Publication date 17 August 2006

Published in The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlap.2005.10.006

zbMATH Keywords

higher-order algebrainfinite systolic algorithmthird-order equational techniques

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical problems of computer architecture (68M07)

Recommendations

• Correctness of dataflow and systolic algorithms using algebras of streams
• Mechanical certification of systolic algorithms
• Automatic verification of a class of systolic circuits
• Algebraic process verification.
• A Mathematical Model for the Verification of Systolic Networks

Cites work

• scientific article; zbMATH DE number 4016180 (Why is no real title available?)
• scientific article; zbMATH DE number 3888893 (Why is no real title available?)
• scientific article; zbMATH DE number 3919789 (Why is no real title available?)
• scientific article; zbMATH DE number 4078770 (Why is no real title available?)
• scientific article; zbMATH DE number 50758 (Why is no real title available?)
• scientific article; zbMATH DE number 1088024 (Why is no real title available?)
• scientific article; zbMATH DE number 1543358 (Why is no real title available?)
• A completeness theorem for the expressive power of higher-order algebraic specifications
• A survey of stream processing
• An algebraic semantics of higher-order types with subtypes
• Correctness of dataflow and systolic algorithms using algebras of streams
• Higher order data types
• Higher-order equational logic for specification, simulation and testing
• On specifications, theories, and models with higher types
• On the power of higher-order algebraic specification methods
• Proving and rewriting
• Specification of abstract data types
• Universal algebra in higher types

Cited in

(3)

• Correctness of dataflow and systolic algorithms using algebras of streams
• Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers
• Unifying computers and dynamical systems using the theory of synchronous concurrent algorithms

Describes a project that uses

Uses Software

• ELAN

This page was built for publication: Verifying an infinite systolic algorithm using third-order equational methods

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2500698)