Téma disertační práce

Školitel:Vojnar Tomáš, prof. Ing., Ph.D.
Téma:Formální verifikace software s využitím teorie automatů
Zahájení v ak.r.:2006/2007
Obhajoba disertace:2011-03-03
Název disertace:Simulations and Antichains for Efficient Handling of Finite Automata
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 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.

Součást výzkumného projektu:
Publikace související s vypsaným tématem:
2006BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam a VOJNAR Tomáš. Abstract Regular Tree Model Checking. Electronic Notes in Theoretical Computer Science. 2006, roč. 149, č. 1, s. 37-48. ISSN 1571-0661.
 ČEŠKA Milan, ERLEBACH Pavel a VOJNAR Tomáš. Pattern-Based Verification of Programs with Extended Linear Linked Data Structures. Electronic Notes in Theoretical Computer Science. 2006, roč. 2006, č. 145, s. 113-130. ISSN 1571-0661.
2005BOUAJJANI Ahmed, HABERMEHL Peter, MORO Pierre a 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, s. 13-29. ISBN 978-3-540-25333-4.
 HABERMEHL Peter a VOJNAR Tomáš. Regular Model Checking Using Inference of Regular Languages. Electronic Notes in Theoretical Computer Science. 2005, roč. 138, č. 3, s. 21-36. ISSN 1571-0661.
 ČEŠKA Milan, KŘENA Bohuslav a VOJNAR Tomáš. Parallel State Space Generation and Exploration on Shared-Memory Architectures. In: Computer Aided Systems Theory - EUROCAST 2005. Berlin: Springer Verlag, 2005, s. 275-280. ISBN 978-3-540-29002-5.
2004BOUAJJANI Ahmed, HABERMEHL Peter a VOJNAR Tomáš. Abstract Regular Model Checking. Lecture Notes in Computer Science. 2004, roč. 2004, č. 3114, s. 372-386. ISSN 0302-9743.

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