Topic of PhD thesis

Advisor:Vojnar Tomáš, prof. Ing., Ph.D.
Student:Fiedor Tomáš, Ing.
Topic:Formal Analysis and Verification of Program Termination and Resource Consumption -- co-supervised by assoc. prof. A. Rogalewicz
Start:2014/2015
PhD thesis subject:

Automatizovaná analýza a verifikace postavená na formálních základech je moderním a rychle se rozvíjejícím přístupem k ověřování korektnosti počítačových systémů, resp. pro vyhledávání chyb v nich. Existuje a dále se rozvíjí mnoho přístupů k takové analýze či verifikaci: nejrůznější formy statické analýzy (analýza toku dat, pokročilé typové analýzy aj.), abstraktní interpretace, model checking apod. Značná pozornost je těmto přístupům věnována nejen v akademické oblasti, ale také řadou špičkových velkých průmyslových společností (např. IBM, Microsoft, Google, NEC apod.) i nově vznikajících spin-off firem (např. Coverity, GrammaTech, MathWorks/AbsInt, Monoidics apod.). Přes tento zájem univerzit i průmyslových společností je však v oblasti analýzy a verifikace stále zapotřebí vyřešit celou řadu teoretických i praktických problémů.

Předmětem disertační práce bude konkrétně rozvoj současného stavu v oblasti automatizované formální analýzy a verifikace konečnosti běhu programů a spotřeby výpočetních zdrojů programy. Důraz by měl být kladen zejména na programy s dynamickými datovými strukturami založenými na ukazatelích či poli s parametrickou velikostí. Za tím účelem budou rozvíjeny techniky založené na použití různých typů automatů (např. automatů nad stromy), logik (separační logika), případně grafů podobně, jako je tomu u nástrojů Forester, Predator či CPAlien vyvíjených skupinou VeriFIT. Výzkum by měl zahrnout nejen teoretický návrh základních principů nových algoritmů analýzy a verifikace, ale i problematiku jejich efektivní implementace a ověření na vhodných případových studiích.

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. A. Rogalewiczem a dr. L. Holíkem. Je zde rovněž možnost úzké spolupráce s různými zahraničními partnery VeriFIT: TU Vídeň, Rakousko (prof. H. Veith, dr. F. Zuleger), Verimag, Grenoble, Francie (dr. R. Iosif), LIAFA, Paříž, Francie (prof. A. Bouajjani, dr. P. Habermehl, dr. M. Sighireanu, dr. C. Enea) či SoSY Lab, University of Passau, Německo (prof. D. Beyer).

Part of research project:
Related publications:
2013ABDULLA Parosh A., HOLÍK Lukáš, JONSSON Bengt, LENGÁL Ondřej, TRINH Quy Cong and VOJNAR Tomáš. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. In: Proceedings of ATVA'13. Heidelberg: Springer Verlag, 2013, pp. 224-239. ISBN 978-3-319-02443-1.
 DUDKA Kamil, PERINGER Petr and VOJNAR Tomáš. Byte-Precise Verification of Low-Level List Manipulation. In: 20th Static Analysis Symposium. Berlin: Springer Verlag, 2013, pp. 215-237. ISBN 978-3-642-38855-2. ISSN 0302-9743.
 HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Fully Automated Shape Analysis Based on Forest Automata. In: Proceedings of CAV'13. Heidelberg: Springer Verlag, 2013, pp. 740-755. ISBN 978-3-642-39798-1. ISSN 0302-9743.
 IOSIF Radu and ROGALEWICZ Adam. Automata-Based Termination Proofs. Computing and Informatics. Bratislava: Slovak Academic Press, 2013, vol. 2013, no. 4, pp. 739-775. ISSN 1335-9150.
2011BOUAJJANI Ahmed, BOZGA Marius, HABERMEHL Peter, IOSIF Radu, MORO Pierre and VOJNAR Tomáš. Programs with Lists are Counter Automata. Formal Methods in System Design. Berlin: Springer Verlag, 2011, vol. 38, no. 2, pp. 158-192. ISSN 0925-9856.
2007HABERMEHL Peter, IOSIF Radu, ROGALEWICZ Adam and VOJNAR Tomáš. Proving Termination of Tree Manipulating Programs. In: Automated Technology for Verification and Analysis. Berlin: Springer Verlag, 2007, pp. 145-161. ISBN 978-3-540-75595-1.