Formal Verification of the CRC Algorithm Properties
| Authors | |
|---|---|
| Year of publication | 2006 |
| Type | Article in Proceedings |
| Conference | Proceedings of 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006) |
| MU Faculty or unit | |
| Citation | |
| Field | Informatics |
| Keywords | formal verification; CRC algorithms; generating polynomial |
| Description | This paper presents verification of the CRC algorithm properties. We examine a way of verifying the CRC algorithm using exhaustive state space exploration by model checking method. The CRC algorithm is used for the calculation of the hash value of a message and we focused to verify the property of finding minimum Hamming distance between two messages having the same hash value. We deal with some of 16, 32 and 64 bits CRC generator polynomials, especially with one used in the Liberouter project, for comparison with others used in the ethernet networking. |
| Related projects: |