Topic of PhD thesis

Advisor:Vojnar Tomáš, prof. Ing., Ph.D.
Student:Janků Petr, Ing.
Topic:Automata in Decision Procedures and Formal Verification -- co-supervised by dr. L. Holik
Start:2015/2016
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 formální verifikace počítačových programů s velmi rozsáhlým, případně nekonečným stavovým prostorem. Důraz bude kladen na symbolickou verifikaci s využitím prostředků teorie formálních jazyků a automatů, případně logik a jejich rozhodovacích procedur založených na automatech.

Práce bude řešena ve spolupráci s týmem VeriFIT zabývajícím se na FIT VUT automatizovanou verifikací, zejména pak dr. L. Holíkem, dr. A. Rogalewiczem, Ing. O. Lengálem a Ing. T. Fiedorem. Je zde rovněž možnost úzké spolupráce s různými zahraničními partnery VeriFIT: Uppsala University, Švédsko (prof. P.A. Abdulla, prof. B. Jonsson); Verimag, Grenoble, Francie (dr. R. Iosif), LIAFA, Paříž, Francie (prof. A. Bouajjani, dr. P. Habermehl, dr. M. Sighireanu, dr. C. Enea), Academia Sinica (prof. Y.-F. Cheng) či TU Vídeň, Rakousko (prof. H. Veith, dr. F. Zuleger). Téma je zajímavé také z pohledu spolupráce se společností Red Hat Czech a jeho laboratoří na FIT VUT.

Part of research project: