Téma disertační práce

Školitel:Vojnar Tomáš, prof. Ing., Ph.D.
Téma:Statická analýza programů se složitými řídicími či datovými strukturami
Zahájení v ak.r.:2016/2017
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 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, dr. 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), Academia Sinica (prof. Y.-F. Chen), TU Keiserslautern, Německo (prof. R. Meyer) či TU Vídeň, Rakousko (prof. H. Veith). Téma je zajímavé také z pohledu spolupráce s průmyslovými společnostmi, jako jsou 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, č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 mimo jiné umožnit verifikaci fragmentů programů bez nutnosti implementovat jejich okolí, verifikovat programy s více zdroji neomezenosti (např. paralelní programy s dynamickými datovými strukturami), zvládnout analýzu paralelních programů využívajících moderní synchronizační technologie (bezzámkové struktury, RCU, Spark apod.), umožnit převod programů se složitými datovými strukturami implementovanými pomocí nízkoúrovňových operací na programy s kontejnery, umožnit analýzu programů s mnoha různými typy dat apod.

Součást výzkumného projektu:
Publikace související s vypsaným tématem:
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.
 MÜLLER Petr, PERINGER Petr a VOJNAR Tomáš. Predator Hunting Party (Competition Contribution). In: Proceedings of TACAS'15. Heidelberg: Springer Verlag, 2015, s. 443-446. ISBN 978-3-662-46680-3.
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.
2013ABDULLA Parosh A., HAZIZA Frédéric, HOLÍK Lukáš, JONSSON Bengt a REZINE Ahmed. An Integrated Specification and Verification Technique for Highly Concurrent Data Structures. In: 19th International Conference, TACAS 2013. Berlin Heidelberg: Springer Verlag, 2013, s. 324-338. ISBN 978-3-642-36742-7. ISSN 0302-9743.
 DUDKA 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: 35.175.191.168
Přepnout na https