Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Correctness of dataflow and systolic algorithms using algebras of streams
KTH, Superseded Departments, Numerical Analysis and Computer Science, NADA.ORCID iD: 0000-0002-9706-5008
2001 (English)In: Acta Informatica, ISSN 0001-5903, E-ISSN 1432-0525, Vol. 38, no 1, 45-88 p.Article in journal (Refereed) Published
Abstract [en]

We present two case studies which illustrate the use of second-order algebra as a formalism for specification and verification of hardware algorithms. In the first case study we specify a systolic algorithm for convolution and formally verify its correctness using second-order equational logic. The second case study demonstrates the expressive power of second-order algebraic specifications by presenting a non-constructive specification of the Hamming stream problem. A dataflow algorithm for computing the Hamming stream is then specified and the correctness of this algorithm is verified by semantical methods. Both case studies illustrate aspects of the metatheory of second-order equational logic.

Place, publisher, year, edition, pages
2001. Vol. 38, no 1, 45-88 p.
Keyword [en]
specifications, completeness, semantics
Identifiers
URN: urn:nbn:se:kth:diva-20982ISI: 000171300700002OAI: oai:DiVA.org:kth-20982DiVA: diva2:339679
Note
QC 20100525Available from: 2010-08-10 Created: 2010-08-10 Last updated: 2017-12-12Bibliographically approved

Open Access in DiVA

No full text

Authority records BETA

Meinke, Karl

Search in DiVA

By author/editor
Meinke, Karl
By organisation
Numerical Analysis and Computer Science, NADA
In the same journal
Acta Informatica

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 29 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf