Topic of PhD thesis

Advisor:Vojnar Tomáš, prof. Ing., Ph.D.
Student:Holík Lukáš, Mgr.
Topic:Formal Verification of Software Using the Automata Theory
Start:2006/2007
Date of Defense:2011-03-03
Title of Dissertation:Simulace a protiřetězce pro efektivní práci s konečnými automaty
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ů využívajících pokročilé programovací techniky (paralelismus, dynamická paměť, sebe-opravování apod.). Programy uvažovaného typu mají obvykle velmi rozsáhlý, případně nekonečný stavový prostor se složitou topologií stavů. V rámci disertační práce budou rozvíjeny stávající a navrženy nové automatizované metody pro vyrovnání se s těmito překážkami. Důraz bude kladen na symbolickou verifikaci s využitím prostředků teorie formálních jazyků a logik, automatizovanou abstrakci a případně metody strojového učení (odvození charakteristik chování systémů ze vzorků tohoto chování).

Práce bude řešena ve spolupráci s týmem VeriFIT zabývajícím se na FIT VUT automatizovanou verifikací. V případě zodpovědného přístupu a kvalitních výsledků je zde možnost zapojení do grantových projektů (včetně zahraničních), získání mimořádné stipendijní podpory i možnost kratších i delších zahraničních stáží na zahraničních pracovištích, s nimiž FIT v dané oblasti spolupracuje.

Part of research project:
Related publications:
2006BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam and VOJNAR Tomáš. Abstract Regular Tree Model Checking. Electronic Notes in Theoretical Computer Science. 2006, vol. 149, no. 1, pp. 37-48. ISSN 1571-0661.
 ČEŠKA Milan, ERLEBACH Pavel and VOJNAR Tomáš. Pattern-Based Verification of Programs with Extended Linear Linked Data Structures. Electronic Notes in Theoretical Computer Science. 2006, vol. 2006, no. 145, pp. 113-130. ISSN 1571-0661.
2005BOUAJJANI Ahmed, HABERMEHL Peter, MORO Pierre and VOJNAR Tomáš. Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. In: Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer Verlag, 2005, pp. 13-29. ISBN 978-3-540-25333-4.
 HABERMEHL Peter and VOJNAR Tomáš. Regular Model Checking Using Inference of Regular Languages. Electronic Notes in Theoretical Computer Science. 2005, vol. 138, no. 3, pp. 21-36. ISSN 1571-0661.
 ČEŠKA Milan, KŘENA Bohuslav and VOJNAR Tomáš. Parallel State Space Generation and Exploration on Shared-Memory Architectures. In: Computer Aided Systems Theory - EUROCAST 2005. Berlin: Springer Verlag, 2005, pp. 275-280. ISBN 978-3-540-29002-5.
2004BOUAJJANI Ahmed, HABERMEHL Peter and VOJNAR Tomáš. Abstract Regular Model Checking. Lecture Notes in Computer Science. 2004, vol. 2004, no. 3114, pp. 372-386. ISSN 0302-9743.