Topic of PhD thesis

Advisor:Vojnar Tomáš, prof. Ing., Ph.D.
Student:Šimáček Jiří, Ing.
Topic:Symbolic Verification Based on Finite Automata and Related Formalisms -- double degree study (cotutelle) with VERIMAG, Grenoble (dr. R. Iosif)
Start:2008/2009
Date of Defense:2012-10-29
Title of Dissertation:Harnessing Forest Automata for Verification of Heap Manipulating Programs
PhD thesis subject:

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).

Part of research project: