Formal Verification of the CRC Algorithm Properties

Warning

This publication doesn't include Faculty of Sports Studies. 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:	Integrated approach to education of PhD students in the area of parallel and distributed systems Institute for Theoretical Computer Science Highly Parallel and Distributed Computing Systems