Topic of PhD thesis

Advisor:Vojnar Tomáš, prof. Ing., Ph.D.
Student:Lengál Ondřej, Ing.
Topic:Efficient Algorithms for Using Automata in Infinite-State Verification -- co-supervised by dr. L. Holik
Start:2010/2011
Date of Defense:2015-07-02
Title of Dissertation:Automata in Infinite-state Formal Verification
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ět disertační práce souvisí s využitím automatů v symbolické formální verifikaci počítačových programů s různými rysy nekonečnosti v datech a/nebo chování, jako jsou např. práce s neomezenými číselnými proměnnými, poli, dynamickými datovými strukturami, rekurzí, paralelismem, parametrizací apod. Konkrétně se jedná o návrh algoritmů a datových struktur umožnujících efektivní práci s různými potřebnými typy automatů (nedeterministické automaty, nedeterministické stromové automaty apod.). Výzkum by měl zahrnout nejen teoretický návrh základních principů takových algoritmů, ale i problematiku jejich vysoce efektivní implementace (včetně využití BDD, možnosti paralelizace apod.) a ověření na vhodných případových studiích.

Práce je řešena ve spolupráci s týmem VeriFIT zabývajícím se na FIT VUT automatizovanou verifikací. Je zde možnost spolupracovat na různých projektech a také s různými zahraničními partnery VeriFIT (Uppsala University; LIAFA, Paříž; University of Edinburgh; Academia Sinica, Taiwan; VERIMAG, Grenoble).

Part of research project:
Related publications:
2009ABDULLA Parosh A., HOLÍK Lukáš, KAATI Lisa and VOJNAR Tomáš. A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. Electronic Notes in Theoretical Computer Science. 2009, vol. 2009, no. 251, pp. 27-48. ISSN 1571-0661.
2008BOUAJJANI Ahmed, HABERMEHL Peter, HOLÍK Lukáš, TOUILI Tayssir and VOJNAR Tomáš. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. FIT-TR-2008-007, Brno: Faculty of Information Technology BUT, 2008.
2007ROGALEWICZ Adam. Verification of Programs with Complex Data Structures. Brno, 2007. ISBN 978-80-214-3548-3.
 VOJNAR Tomáš. Cut-offs and Automata in Formal Verification of Infinite-State Systems. Brno: Faculty of Information Technology BUT, 2007. ISBN 978-80-214-3547-6.