Téma disertační práce

Školitel:Vojnar Tomáš, prof. Ing., Ph.D.
Téma:Symbolická verifikace s využitím konečných automatů a příbuzných formalismů -- společné vedení (double degree/cotutelle) s VERIMAG, Grenoble (dr. R. Iosif)
Zahájení v ak.r.:2008/2009
Obhajoba disertace:2012-10-29
Název disertace:Verifikace Programů se složitými datovými strukturami
Charakteristika řešeného problému:

Automatizovaná formální verifikace je moderním a rychle se rozvíjejícím přístupem k ověřování korektnosti počítačových systémů. Značná pozornost je jí věnována nejen v akademické oblasti, ale také řadou špičkových průmyslových společností působících v oblasti hardware (např. Intel, IBM), počítačových protokolů a sítí, vestavěných řídících systémů (např. pro potřeby palubních řídících systémů NASA) a v neposlední řadě také operačních systémů (zde se v současnosti stále více angažuje firma Microsoft a její divize Microsoft Research). Přes tento zájem univerzit i průmyslových společností je však v oblasti formální verifikace stále zapotřebí vyřešit celou řadu teoretických i praktických problémů.

Předmětem disertační práce je konkrétně formální verifikace počítačových programů s různými rysy nekonečnosti v datech a/nebo chování, zejména pak programů s dynamickými datovými strukturami propojenými ukazateli. Důraz bude kladen na rozvoj metod symbolické verifikace s cílem zvýšit její obecnost a efektivnost, a to zejména při využití konečných automatů, konečných stromových automatů a jejich různých rozšíření. Alternativně může být studováno též využití jiných formalismů, např. různých typů logik.

Práce je řešena ve spolupráci s týmem VeriFIT zabývajícím se na FIT VUT automatizovanou verifikací. Jedná se přitom o dvojí vedení (cotutelle/double degree) s VERIMAG, Grenoble (dr. R. Iosif).

Součást výzkumného projektu:

Vaše IPv4 adresa: 35.175.191.168
Přepnout na https