Towards efficient verification of arithmetic algorithms over galois fields GF(2m)

18Citations
Citations of this article
2Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

The Galois field GF(2m) is an important number system that is widely used in applications such as error correction codes (ECC), and complicated combinations of arithmetic operations are performed in those applications. However, few practical formal methods for algorithm verification at the word-level have ever been developed. We have defined a logic system, (formula presented) -arithmetic, that can treat non-linear and non-convex constraints, for describing specifications and implementations of arithmetic algorithms over GF(2m). We have investigated various decision techniques for the (formula presented) -arithmetic and its subclasses, and have performed an automatic correctness proof of a (n, n 4) Reed-Solomon ECC decoding algorithm. Because the correctness criterion is in an efficient subclass of the (formula presented) -arithmetic (k -field-size independent), the proof is completed in significantly reduced time, less than one second for any m ≥ 3 and n ≥ 5, by using a combination of polynomial division and variable elimination over GF(2m), without using any costly techniques such as factoring or a decision over GF(2) that can easily increase the verification time to more than a day.

Cite

CITATION STYLE

APA

Morioka, S., Katayama, Y., & Yamane, T. (2001). Towards efficient verification of arithmetic algorithms over galois fields GF(2m). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2102, pp. 465–477). Springer Verlag. https://doi.org/10.1007/3-540-44585-4_45

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free