ŠAFRÁNEK, David, Vojtěch ŘEHÁK, Tomáš KRATOCHVÍLA, Pavel ŠIMEČEK, Petr HLÁVKA a Tomáš VOJNAR. CRC64 Algorithm Analysis and Verification. Brno: CESNET, z. s. p. o. Technical Report 27/2005. 2005.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název CRC64 Algorithm Analysis and Verification
Název česky CRC64 Algorithm Analysis and Verification
Autoři ŠAFRÁNEK, David (203 Česká republika, garant), Vojtěch ŘEHÁK (203 Česká republika), Tomáš KRATOCHVÍLA (203 Česká republika), Pavel ŠIMEČEK (203 Česká republika), Petr HLÁVKA (203 Česká republika) a Tomáš VOJNAR (203 Česká republika).
Vydání Brno, Technical Report 27/2005, 2005.
Nakladatel CESNET, z. s. p. o.
Další údaje
Originální jazyk angličtina
Typ výsledku Audiovizuální tvorba
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Česká republika
Utajení není předmětem státního či obchodního tajemství
WWW URL
Kód RIV RIV/00216224:14330/05:00012922
Organizační jednotka Fakulta informatiky
Klíčová slova anglicky CRC64; formal verification; correctness of CRC algorithm
Štítky correctness of CRC algorithm, CRC64, formal verification
Změnil Změnil: RNDr. Pavel Šimeček, Ph.D., učo 51636. Změněno: 2. 5. 2008 13:57.
Anotace
This work analyzes the use of a CRC64 algorithm as a hashing function in the Netflow project. We describe the basis of Cyclic Redundancy Check (CRC) algorithms and consider properties like collision probability, Hamming distance, and quality of distribution, which are crucial for hashing functions. Lower or upper bounds of these properties are described mathematically. However, to give more precise numbers to hardware designers, we also try to find them using model checking method.
Anotace česky
Zpráva obsahuje analýzu a verifikaci algoritmu implementovaného v hardware pro kontrolní součet CRC64. Základy algoritmu CRC jsou popsány v první části právce, po té jsou stanoveny klíčové vlastnosti zaručující korektnost - pravděpodobnost kolize, Hammingova vzálenost a kvalita distribuce hašujících funkcí.
Návaznosti
GA201/03/0509, projekt VaVNázev: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Automatizovaná verifikace paralelních a distribuovaných systémů
GD102/05/H050, projekt VaVNázev: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1ET408050503, projekt VaVNázev: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů
VytisknoutZobrazeno: 29. 3. 2024 07:53