Distributed LTL Model Checking with Hash Compaction

Základní údaje

Originální název Distributed LTL Model Checking with Hash Compaction
Název česky Distribuované ověřování modelů LTL za pomoci hash compaction
Autoři

Další údaje

Citace BARNAT, Jiří, Jan HAVLÍČEK a Petr ROČKAI. Distributed LTL Model Checking with Hash Compaction. In Electronic Notes in Theoretical Computer Science, Volume 296. Neuveden: Elsevier Science, 2013. s. 79-93, 15 s. ISSN 1571-0661. doi:10.1016/j.entcs.2013.07.006.
Originální jazyk angličtina
Obor Informatika
WWW
Druh Článek ve sborníku
Klíčová slova model checking; LTL; hash compaction

Anotace

Rozšiřujeme distribuovaný algoritmus OWCTY pro realizaci verifikační metody enumerativní ověřování modelu o možnost uchovávat navštívené stavy pouze jako jejich otisky z hashovací funkce. Podáváme detailní popis algoritmu a důkaz korektnosti. Součástí výsledku je implementace algoritmu v prostředí verifikačního nástroje DIVINE a experimentální vyhodnocení.

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info