Informatické kolokvium 19. 4. 10 let nástroje DIVINE – Co bylo, je a bude
Informatické kolokvium 19. 4. 2016, 14:00 posluchárna D2
doc. RNDr. Jiří Barnat, Ph.D., FI MU
10 let nástroje DIVINE – Co bylo, je a bude
Abstrakt: Technika zvaná ověřování modelu (angl. Model Checking) je v centru zájmu komunity vědců zabývající se automatizovanou formální verifikací již déle jak čtvrt století. Přestože za tuto dobu bylo vymyšleno mnoho vylepšení a řada nových technik, které výrazně posouvají možnosti této metody formální verifikace, její penetrace do běžného industriálního informatického života je výrazně menší, než se zpočátku čekalo. Cílem přednášky je shrnout zkušenosti s vývojem a používáním verifikačního nástroje DIVINE, který stojí na metodě enumerativního ověřování modelu. V přednášce krátce zrekapitulujeme výsledky, kterých bylo v souvislosti s vývojem nástrojem DIVINE dosaženo, zhodnotíme jejich silné a slabé stránky a nastíníme směr, kterým se bude vývoj nástroje DIVINE ubírat v blízké budoucnosti.
doc. RNDr. Jiří Barnat, Ph.D., FI MU
10 let nástroje DIVINE – Co bylo, je a bude
Abstrakt: Technika zvaná ověřování modelu (angl. Model Checking) je v centru zájmu komunity vědců zabývající se automatizovanou formální verifikací již déle jak čtvrt století. Přestože za tuto dobu bylo vymyšleno mnoho vylepšení a řada nových technik, které výrazně posouvají možnosti této metody formální verifikace, její penetrace do běžného industriálního informatického života je výrazně menší, než se zpočátku čekalo. Cílem přednášky je shrnout zkušenosti s vývojem a používáním verifikačního nástroje DIVINE, který stojí na metodě enumerativního ověřování modelu. V přednášce krátce zrekapitulujeme výsledky, kterých bylo v souvislosti s vývojem nástrojem DIVINE dosaženo, zhodnotíme jejich silné a slabé stránky a nastíníme směr, kterým se bude vývoj nástroje DIVINE ubírat v blízké budoucnosti.