Other formats:
BibTeX
LaTeX
RIS
@inproceedings{701731, author = {Smrčka, Aleš and Hlávka, Petr and Šafránek, David and Řehák, Vojtěch and Šimeček, Pavel and Vojnar, Tomáš}, address = {Brno}, booktitle = {Proceedings of 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006)}, keywords = {formal verification; CRC algorithms; generating polynomial}, language = {eng}, location = {Brno}, isbn = {80-214-3287-X}, pages = {55-62}, publisher = {FIT BUT}, title = {Formal Verification of the CRC Algorithm Properties}, year = {2006} }
TY - JOUR ID - 701731 AU - Smrčka, Aleš - Hlávka, Petr - Šafránek, David - Řehák, Vojtěch - Šimeček, Pavel - Vojnar, Tomáš PY - 2006 TI - Formal Verification of the CRC Algorithm Properties PB - FIT BUT CY - Brno SN - 802143287X KW - formal verification KW - CRC algorithms KW - generating polynomial N2 - 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. ER -
SMRČKA, Aleš, Petr HLÁVKA, David ŠAFRÁNEK, Vojtěch ŘEHÁK, Pavel ŠIMEČEK and Tomáš VOJNAR. Formal Verification of the CRC Algorithm Properties. In \textit{Proceedings of 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006)}. Brno: FIT BUT, 2006, p.~55-62. ISBN~80-214-3287-X.
|