Topic of PhD thesis

Advisor:Vojnar Tomáš, prof. Ing., Ph.D.
Student:Turoňová Lenka, Ing.
Topic:Formal Verification of Concurrent Programs with an Unbounded Number of Concurrent Threads -- co-supervised by dr. L. Holik
Start:2015/2016
PhD thesis subject:

Formální analýza a verifikace 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: analýza toku dat, pokročilé typové analýzy, 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, Red Hat, Facebook 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 statické analýzy 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 formální analýzy a verifikace programů s neomezeným počtem paralelně běžících výpočetních vláken, případně i jiných typů paralelních systémů s neomezeným stupněm paralelismu (jako jsou např. komunikační protokoly, návrh hardwarových systémů ve vysoko-úrovňových jazycích pro popis hardware apod.)

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.

V oblasti formální analýzy a verifikace systémů s neomezeným počtem paralelně běžících výpočetních vláken má skupina VeriFIT bohaté zkušenost zahrnující využití technik jako jsou řezy (cut-offs), regulární model checking či tzv. pohledová abstrakce (view abstraction). Cílem disertační práce bude posunout současný stav v této oblasti k vyšší efektivitě, obecnosti a/nebo vyššímu stupni automatizace současných přístupů. V rámci toho by měly být studovány např. možnosti verifikace systémů kombinující neomezený paralelismus s dalšími zdroji neomezenosti, a to zejména dynamickými datovými strukturami použitými např. bezzámkovým způsobem, s použitím technologií jako jsou transakční paměti, a/nebo v kontextu tzv. slabých paměťových modelů zajišťujících pouze částečné uspořádání zápisů do paměti. Práce by se měla přitom zaměřit nejen na verifikaci dosud převážně studovaných vlastností typu bezpečnost, ale měla by uvážit také vlastnosti typu živost. Budou přitom používány a dále rozvíjeny zejména prostředky z oblasti teorie automatů a logik.

Part of research project:
Related publications:
2014ABDULLA Parosh A., HAZIZA Frédéric and HOLÍK Lukáš. Block Me If You Can! Context-Sensitive Parameterized Verification. In: 21st International Static Analysis Symposium. Berlin: Springer Verlag, 2014, pp. 1-17. ISBN 978-3-319-10935-0. ISSN 0302-9743.
 CHARVÁT Lukáš, SMRČKA Aleš and VOJNAR Tomáš. Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors. In: Proceedings of 15th International Workshop on Microprocessor Test and Verification (MTV 2014). Austin, TX: IEEE Computer Society, 2014, pp. 83-89. ISBN 978-1-4673-6858-2.
2013ABDULLA Parosh A., HAZIZA Frédéric and HOLÍK Lukáš. All for the Price of Few (Parameterized Verification through View Abstraction). In: Proc. of VMCAI 2013. Berlin Heidelberg: Springer Verlag, 2013, pp. 476-495. ISBN 978-3-642-35872-2. ISSN 0302-9743.
 ABDULLA Parosh A., HAZIZA Frédéric, HOLÍK Lukáš, JONSSON Bengt and REZINE Ahmed. An Integrated Specification and Verification Technique for Highly Concurrent Data Structures. In: 19th International Conference, TACAS 2013. Berlin Heidelberg: Springer Verlag, 2013, pp. 324-338. ISBN 978-3-642-36742-7. ISSN 0302-9743.
 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.
2012BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam and VOJNAR Tomáš. Abstract Regular (Tree) Model Checking. International Journal on Software Tools for Technology Transfer. 2012, vol. 14, no. 2, pp. 167-191. ISSN 1433-2779.
2007VOJNAR 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.