Informace o projektu
Rozšířená verifikace konečně stavových systémů

Projekt je zaměřen na návrh a verifikaci počítačových systémů pomocí matematických modelů, konkrétně metodou "ověřování modelů" (model checking). Tato metoda zkoumá všechna možná chování systému a je tedy daleko spolehlivější než klasické, neúplné metody (testování, simulace). Je však také výrazně výpočetně náročnější. Cílem projektu je rozšíření této metody ve třech směrech: algoritmická rozšíření (náhodnostní, paralelní), rozšíření automatizace procesu verifikace, rozšíření informací poskytovaných uživateli zejména o kvantitativní informace.