Topic of PhD thesis

Advisor:Vojnar Tomáš, prof. Ing., Ph.D.
Topic:Static Formal Analysis of Programs with Advanced Data and Control Structures
Start:2018/2019
PhD thesis subject:

Statická analýza 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: 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, Amazon apod.) i nově vznikajících spin-off firem (např. Coverity, GrammaTech, AbsInt, DiffBlue 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 statické analýzy zaměřené na programy se složitými řídicími a/nebo datovými strukturami: zvýšení obecnosti těchto technik, zvýšení jejich škálovatelnosti, zlepšení stupně automatizace.

Práce bude řešena ve spolupráci s týmem VeriFIT zabývajícím se na FIT VUT automatizovanou analýzou a verifikací, zejména pak dr. L. Holíkem, doc. A. Rogalewiczem, dr. O. Lengálem, dr. P. Peringerem, Ing. T. Fiedorem, Ing. M. Hruškou, Ing. V. Šokovou či Ing. V. Malíkem. 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, dr. Rummer); Verimag, Grenoble, Francie (dr. R. Iosif), IRIF, Paříž, Francie (prof. A. Bouajjani, dr. M. Sighireanu, dr. C. Enea), Academia Sinica, Tchaj-wan (prof. Y.-F. Chen), TU Vienna, Rakousko (dr. F. Zuleger), University of Oxford, Velká Británie (dr. A.W. Lin) či TU Braunschweig, Německo (prof. R. Meyer). Téma je zajímavé také z pohledu spolupráce s průmyslovými společnostmi, zejména pak DiffBlue z Velké Británie (dr. P. Schrammel), která vyvíjí mj. statický analyzátor 2LS, do jehož vývoje se již tým VeriFIT zapojil v několika oblastech. Dalšími možnými průmyslovými partnery jsou např. Red Hat či Honeywell.

V oblasti statické analýzy programů dosáhla skupina VeriFIT mnoha originálních výsledků publikovaných na špičkových konferencích (např. v oblasti analýzy programů s dynamickými datovými strukturami, parametrickými datovými strukturami, neomezenými poli, řetězci či parametrickým počtem procesů). Řada z dosažených výsledků byla implementována v nástrojích (např. Predator či Forester), které získaly řadu ocenění např. na mezinárodní soutěži ve verifikaci software SV-COMP. Konkrétní výzkum v rámci tématu se zaměří na další významné zdokonalení metod, na nichž tyto nástroje stojí, ať už se jedná o techniky založené na automatech, logikách či grafech. Cílem bude např. umožnit efektivní analýzu programů s více různými typy dat (např. ukazatele a celočíselné proměnné), navrhnout nové techniky analýzy programů s dynamickými datovými strukturami (např. s využitím analýzy založené na šablonách a vazby na řešení SAT/SMT problémů), umožnit efektivní verifikaci konečnosti a nekonečnosti běhu programů či automatickou analýzu složitosti, umožnit verifikaci fragmentů kódu, umožnit verifikaci paralelních programů, kde každé jednotlivé vlákno má neomezený stavový prostor či také kombinovat různé (omezené) statické a dynamické analýzy programů za účelem efektivního vyhledávání chyb v nich.

V rámci tématu se student může také aktivně zapojit do různých grantových projektů, jako je např. projekt GA ČR Robust či evropský projekt H2020 ECSEL Aquas.

Part of research project:
Related publications:
2018FIEDOR Tomáš, HOLÍK Lukáš, ROGALEWICZ Adam, SINN Moritz, VOJNAR Tomáš and ZULEGER Florian. From Shapes to Amortized Complexity. In: Proceedings of VMCAI'18. Heidelberg: Springer Verlag, 2018, pp. 205-225. ISBN 978-3-319-73720-1. ISSN 0302-9743.
2017DIAS Ricardo J., FERREIRA Carla, FIEDOR Jan, LOURENCO Joao, SMRČKA Aleš, SOUSA Diogo J. and VOJNAR Tomáš. Verifying Concurrent Programs Using Contracts. In: 2017 IEEE International Conference on Software Testing, Verification and Validation (ICST). Tokyo: Institute of Electrical and Electronics Engineers, 2017, pp. 196-206. ISBN 978-1-5090-6032-0.
 ENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela and VOJNAR Tomáš. SPEN: A Solver for Separation Logic. In: Proceedings of NFM'17. Heidelberg: Springer Verlag, 2017, pp. 302-309. ISBN 978-3-319-57287-1.
 HOLÍK Lukáš, HRUŠKA Martin, LENGÁL Ondřej, ROGALEWICZ Adam and VOJNAR Tomáš. Counterexample Validation and Interpolation-Based Refinement for Forest Automata. In: Proceedings of VMCAI'17. Cham: Springer Verlag, 2017, pp. 288-309. ISBN 978-3-319-52234-0. ISSN 0302-9743.
 HOLÍK Lukáš, MEYER Roland, VOJNAR Tomáš and WOLF Sebastian. Effect Summaries for Thread-Modular Analysis. In: SAS 2017: Static Analysis. Cham: Springer International Publishing, 2017, pp. 169-191. ISBN 978-3-319-66706-5.
2016DUDKA Kamil, HOLÍK Lukáš, PERINGER Petr, TRTÍK Marek and VOJNAR Tomáš. From Low-Level Pointers to High-Level Containers. In: Verification, Model Checking, and Abstract Interpretation (VMCAI). Berlin Heidelberg: Springer Verlag, 2016, pp. 431-452. ISBN 978-3-662-49121-8.
 HOLÍK Lukáš, KOTOUN Michal, PERINGER Petr, ŠOKOVÁ Veronika, TRTÍK Marek and VOJNAR Tomáš. Predator Shape Analysis Tool Suite. In: Proceedings of HVC 2016. Zurich: Springer Verlag, 2016, pp. 202-209. ISBN 978-3-319-49052-6.
2015ABDULLA 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. Acta Informatica. 2015, vol. 53, no. 4, pp. 357-385. ISSN 0001-5903.
2013DUDKA 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.

Vaše IPv4 adresa: 35.173.47.43