FIT A218 11.3.2010

Dudka Kamil: Automatizovaná formální verifikace v operačních systémech
Prezentace se bude zabývat využitím separační logiky pro verifikaci programů, které manipulují s dynamickými datovými strukturami. Bude také stručně představen nástroj Predator, který tuto verifikační metodu implementuje ve formě zásuvného modulu pro překladač gcc a tím umožňuje verifikovat programy v době překladu.

Gach Marek: Verifikace systémů pracujících v reálném čase
Běžné používané metody pro verifikaci programů bez časových omezení lze sice s menšími úpravami použít pro verifikaci systémů s časovými omezeními, nicméně jejich efektivita není nejlepší. Na vině je paralelní kompozice procesů a taktéž zanesení do stavové informace diskretizovaného času. Aktuálně vyvíjený a testovaný přístup je založena na využití techniky popisu a verifikace systémů pomocí Restricted Real-Time Logic (RRTL). Všechny tyto postupy pro Modechart jsou součástí aktuálně vyvíjeného nástroje VERIF, který bude vykázan jako software.

Fiedor Jan: Praktické metody automatizované verifikace paralelních programů
Práce se zabývá výzkumem metod pro verifikaci paralelních programů. Budou stručně shrnuty poznatky právě dokončené rozsáhlé technické zprávy zabývající se klasifikací chyb v paralelních programech a stávajícími metodami jejich detekce. Blíže budou zmíněny některé méně studované typy chyb a nastíněny možnosti jejich řešení.