FIT A112 7.10.2010

Smrčka Aleš: Verifikace asynchronních a parametrických návrhů hardware
Na semináři budou prezentovány dva originální přístupy k formální verifikaci návrhů hardware. První přístup se věnuje použití metody model checking systémů s více hodinovými signály. Budou představeny čtyři metody, které jsou použity pro modelování křížení časových domén takovým způsobem, že následný model checking je schopný odhalit problémy plynoucí ze synchronizace dat. Navrhované metody se liší v přesnosti a v nárocich na formální verifikaci. Další přínos se věnuje verifikaci parametrických návrhů hardware založené na překladu HW návrhu do čítačových automatů. Model získaný tímto způsobem může být verifikován pro všechny hodnoty parametrů najednou.

Holík Lukáš: Simulace a antiřetězce pro efektivní práci s konečnými automaty
Cílem prezentované disertační práce je vývoj technik umožnujících praktické využití nedeterministických konecných automatu, zejména nedeterministických stromových automatu. Jde zvlášte o techniky pro redukci velikosti a testování jazykové inkluze, jež hrají zásadní roli v mnoha oblastech aplikace konecných automatu.