Formal Verification of the CRC Algorithm Properties

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

SMRČKA Aleš HLÁVKA Petr ŠAFRÁNEK David ŘEHÁK Vojtěch ŠIMEČEK Pavel VOJNAR Tomáš

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

Faculty of Informatics

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:

You are running an old browser version. We recommend updating your browser to its latest version.