Towards Efficient Verification of Arithmetic Algorithms over Galois Fields GF(2^m)

Sumio Morioka, Yasunao Katayama, Toshiyuki Yamane

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


Although Galois field GF(2^m) is an important number system that is widely used in applications such as error correction codes, few practical formal verification methodologies have ever been developed. We have defined a logic, GF2^m-arithmetic, that can treat nonlinear and non-convex constraints, for describing specifications and implementations of arithmetic algorithms over GF(2^m). We have investigated various techniques for decision procedures over the GF2^m-arithmetic and/or its sub-classes. By using a combination of polynomial division and variable elimination over GF(2^m), we have carried out automatic correctness proof of a practical (n,n-4)Reed-Solomon decoding algorithm in significantly reduced time, less than 1 second for any m>=3 and n>=5, without using any costly techniques such as factoring or decision over GF(2) that can easily increase the verification time to more than a day.

Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Start Conference Manager
Conference Systems