Téma disertační práce

Školitel:Vojnar Tomáš, prof. Ing., Ph.D.
Téma:Statická analýza a vyhledávání chyb v programech
Zahájení v ak.r.:2017/2018
Charakteristika řešeného problému:

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, MathWorks/AbsInt, Monoidics, 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.

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. 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. M. Sighireanu), Academia Sinica (prof. Y.-F. Chen) či TU Braunschweig, Německo (prof. R. Meyer). Téma je zajímavé také z pohledu spolupráce s průmyslovými společnostmi, jako jsou Red Hat, Honeywell či DiffBlue.

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, č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 mj. umožnit efektivní analýzu programů s více různými typy dat (např. ukazatele a celočíselné proměnné), navhrnou nové techniky analýzy programů s dynamickými datovými strukturami (např. s využitím analýzy založené na šablonách), umožnit efektivní verifikaci konečnosti a nekonečnosti běhu programů, 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.

Součást výzkumného projektu:
Publikace související s vypsaným tématem:
2016DUDKA Kamil, HOLÍK Lukáš, PERINGER Petr, TRTÍK Marek a VOJNAR Tomáš. From Low-Level Pointers to High-Level Containers. In: Verification, Model Checking, and Abstract Interpretation (VMCAI). Berlin Heidelberg: Springer Verlag, 2016, s. 431-452. ISBN 978-3-662-49121-8.
2015ABDULLA Parosh A., HOLÍK Lukáš, JONSSON Bengt, LENGÁL Ondřej, TRINH Quy Cong a VOJNAR Tomáš. Verification of heap manipulating programs with ordered data by extended forest automata. Acta Informatica. 2015, roč. 53, č. 4, s. 357-385. ISSN 0001-5903.
 FIEDOR Jan, LETKO Zdeněk, LOURENCO Joao a VOJNAR Tomáš. Dynamic Validation of Contracts in Concurrent Code. In: Proceedings of EUROCAST'15. Heidelberg: Springer Verlag, 2015, s. 555-564. ISBN 978-3-319-27339-6.
2014ABDULLA Parosh A., HAZIZA Frédéric a HOLÍK Lukáš. Block Me If You Can! Context-Sensitive Parameterized Verification. In: 21st International Static Analysis Symposium. Berlin: Springer Verlag, 2014, s. 1-17. ISBN 978-3-319-10935-0. ISSN 0302-9743.
2013DUDKA Kamil, PERINGER Petr a VOJNAR Tomáš. Byte-Precise Verification of Low-Level List Manipulation. In: 20th Static Analysis Symposium. Berlin: Springer Verlag, 2013, s. 215-237. ISBN 978-3-642-38855-2. ISSN 0302-9743.
 HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří a VOJNAR Tomáš. Fully Automated Shape Analysis Based on Forest Automata. In: Proceedings of CAV'13. Heidelberg: Springer Verlag, 2013, s. 740-755. ISBN 978-3-642-39798-1. ISSN 0302-9743.

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