Name
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, GF2m -arithmetic, that can treat non-linear and nonconvex constraints, for describing specifications and implementations of arithmetic algorithms over GF(2m). We have investigated various decision techniques for the GF2m -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 GF2m -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. |
Year | DOI | Venue |
|---|---|---|
2001 | 10.1007/3-540-44585-4_45 | CAV |
Keywords | Field | DocType |
automatic correctness proof,towards efficient verification,algorithm verification,various decision technique,correctness criterion,verification time,logic system,reed-solomon ecc decoding algorithm,arithmetic algorithm,important number system,arithmetic operation,arithmetic algorithms,galois fields gf,formal method,variable elimination,reed solomon,galois field,error correction code | Discrete mathematics,Finite field,Variable elimination,Computer science,Correctness,Polynomial long division,Algorithm,Arithmetic,Galois theory,GF(2),Mathematics of cyclic redundancy checks,Formal verification | Conference |
Volume | ISSN | ISBN |
2102 | 0302-9743 | 3-540-42345-1 |
Citations | PageRank | References |
13 | 1.55 | 9 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sumio Morioka | 1 | 493 | 45.23 |
| Yasunao Katayama | 2 | 85 | 17.18 |
| Toshiyuki Yamane | 3 | 61 | 9.08 |